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

Merge pull request #449 from ywata/emacs-unicode

Browse source 
Mentioning emacs unicode command #448
This commit is contained in:
Philip Wadler 2020-01-10 11:38:56 -03:00 committed by GitHub
commit 170496699b
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
2 changed files with 37 additions and 4 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
each chapter should provide a list of the unicode characters introduced in that
chapter. For a full list of supported characters, see
[agda-input.el](https://github.com/agda/agda/blob/master/src/data/emacs-mode/agda-input.el#L194).
chapter.
`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`

22
src/plfa/part1/Naturals.lagda.md
View file

@ -965,8 +965,8 @@ After typing `\r`, one can access the many available arrows by using
the left, right, up, and down keys to navigate. The command remembers
where you navigated to the last time, and starts with the same
character next time. The command `\l` works similarly for left arrows.
In place of left, right, up, and down keys, one may also use control characters:
In place of left, right, up, and down keys, one may also use control
characters:
C-b left (backward one character)
C-f right (forward one character)
@ -975,3 +975,21 @@ In place of left, right, up, and down keys, one may also use control characters:
We write `C-b` to stand for control-b, and similarly. One can also navigate
left and right by typing the digits that appear in the displayed list.
For a full list of supported characters, use `agda-input-show-translations` with:
M-x agda-input-show-translations
All the characters supported by `agda-mode` are shown. We write M-x to stand for
typing `ESC` followed by `x`.
If you want to know how you input a specific Unicode character in an agda file,
move the cursor onto the character and use `quail-show-key` with:
M-x quail-show-key
You'll see a key sequence of the character in mini buffer.
If you run `M-x qualy-show-key` on say `∸`, you will see `\.-` for the character.
We write `C-b` to stand for control-b, and similarly. One can also navigate
left and right by typing the digits that appear in the displayed list.