michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Mention some emacs commands.

Browse source
This commit is contained in:
YASUHIKO WATANABE 2020-01-10 23:18:41 +09:00
parent 95fa648a23
commit eb68d083a7
1 changed files with 17 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
README.md
View file

@ -58,8 +58,23 @@ but Aquamacs users might need to move their startup settings to the Preferences.
If you're having trouble typing the Unicode characters into Emacs, the end of If you're having trouble typing the Unicode characters into Emacs, the end of
each chapter should provide a list of the unicode characters introduced in that each chapter should provide a list of the unicode characters introduced in that
chapter. For a full list of supported characters, see chapter.
[agda-input.el](https://github.com/agda/agda/blob/master/src/data/emacs-mode/agda-input.el#L194).
`agda-mode` and emacs have a number of useful commands.
Two of them are especially useful when you solve exercises.
For a full list of supported characters, use `agda-input-show-translations` with:
M-x agda-input-show-translations
All the supported characters in `agda-mode` are shown.
If you want to know how you input a specific Unicode character in agda file,
move the cursor onto the character and type the following command:
M-x quail-show-key
You'll see the key sequence of the character in mini buffer.
## Using `agda-mode` ## Using `agda-mode`