diff options
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 ;; |