diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2010-08-18 10:43:58 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2010-08-18 10:43:58 +0000 |
| commit | 1c896e20c909954df3aad34c5cca1a11c21d40eb (patch) | |
| tree | 2ae9d27a1b7a584436c96b2e13ed89b475aa412f /isar/isar.el | |
| parent | 3160b7ed3fd325c0ae3ea41dc9aeded97556a2ed (diff) | |
Add command bound to C-c C-a h ? to show available help keys
Diffstat (limited to 'isar/isar.el')
| -rw-r--r-- | isar/isar.el | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/isar/isar.el b/isar/isar.el index 2ab4ea88..b4150b98 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -327,8 +327,6 @@ This is called when Proof General spots output matching ;; Help menu ;; -;;; da: how about a `C-c C-a h ?' for listing available keys? - ;;; NB: definvisible must be after derived modes (uses isar-mode-map) (proof-definvisible isar-help-antiquotations "print_antiquotations" "hA") @@ -345,6 +343,12 @@ This is called when Proof General spots output matching (proof-definvisible isar-help-theorems "print_theorems" "ht") (proof-definvisible isar-help-trans-rules "print_trans_rules" "hT") +(define-key isar-mode-map "\C-c\C-ah?" 'isar-describe-help-keys) +(defun isar-describe-help-keys () + "Describe key bindings with prefix C-c C-a h" + (interactive) + (describe-bindings "\C-c\C-ah")) + ;; ;; Command menu ;; |