From eb68d083a763cfd4f1b12052463bdf45a1e2d662 Mon Sep 17 00:00:00 2001
From: YASUHIKO WATANABE <Yasuhiko Watanabe>
Date: Fri, 10 Jan 2020 23:18:41 +0900
Subject: [PATCH 1/3] Mention some emacs commands.
---
README.md | 19 +++++++++++++++++--
1 file changed, 17 insertions(+), 2 deletions(-)
diff --git a/README.md b/README.md
index 19690292..03d9c902 100644
--- a/README.md
+++ b/README.md
@@ -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`
From 6b8e61c1e7b650387e671593cd6f4be710b12c49 Mon Sep 17 00:00:00 2001
From: YASUHIKO WATANABE <Yasuhiko Watanabe>
Date: Fri, 10 Jan 2020 23:19:33 +0900
Subject: [PATCH 2/3] Mention emacs commands in Unicode section.
---
src/plfa/part1/Naturals.lagda.md | 23 ++++++++++++++++++++++-
1 file changed, 22 insertions(+), 1 deletion(-)
diff --git a/src/plfa/part1/Naturals.lagda.md b/src/plfa/part1/Naturals.lagda.md
index dc9cea37..15bf9e9f 100644
--- a/src/plfa/part1/Naturals.lagda.md
+++ b/src/plfa/part1/Naturals.lagda.md
@@ -966,7 +966,28 @@ 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:
+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.
+
+
+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.
+
+How you input the above commands varies according to system and configuration.
+The most portable way would be to type `ESC`, `x` and then type
+`agda-input-show-translations` or `quail-show-key` literally.
+
+It is important to be familiar with moving cursor in `agda-mode`. 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)
From 896b2b528a98da51545f3fb267df673718048787 Mon Sep 17 00:00:00 2001
From: Philip Wadler <wadler@inf.ed.ac.uk>
Date: Fri, 10 Jan 2020 11:38:28 -0300
Subject: [PATCH 3/3] Further edits
I rearranged the material. It is important that control characters for arrows appear next to the description of arrows.
---
src/plfa/part1/Naturals.lagda.md | 41 +++++++++++++++-----------------
1 file changed, 19 insertions(+), 22 deletions(-)
diff --git a/src/plfa/part1/Naturals.lagda.md b/src/plfa/part1/Naturals.lagda.md
index 15bf9e9f..1444ecd9 100644
--- a/src/plfa/part1/Naturals.lagda.md
+++ b/src/plfa/part1/Naturals.lagda.md
@@ -965,28 +965,7 @@ 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.
-
-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.
-
-
-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.
-
-How you input the above commands varies according to system and configuration.
-The most portable way would be to type `ESC`, `x` and then type
-`agda-input-show-translations` or `quail-show-key` literally.
-
-It is important to be familiar with moving cursor in `agda-mode`. In
-place of left, right, up, and down keys, one may also use control
+In place of left, right, up, and down keys, one may also use control
characters:
C-b left (backward one character)
@@ -996,3 +975,21 @@ 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.