From eb68d083a763cfd4f1b12052463bdf45a1e2d662 Mon Sep 17 00:00:00 2001 From: YASUHIKO WATANABE Date: Fri, 10 Jan 2020 23:18:41 +0900 Subject: [PATCH] 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`