aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--generic/proof-menu.el7
-rw-r--r--isar/isar.el2
2 files changed, 8 insertions, 1 deletions
diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index 8ebb0f09..0357180a 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -167,7 +167,12 @@ without adjusting window layout."
(vector
(concat "Exit " proof-assistant)
'proof-shell-exit
- ':active '(proof-shell-live-buffer)))
+ ':active '(proof-shell-live-buffer))
+ ;; TODO: doc <PA>-set-command here
+ (vector
+ (concat "Set " proof-assistant " command")
+ (proof-ass-sym set-command)
+ ':active '(fboundp (proof-ass-sym set-command))))
'("----")
(list
(cons "Help"
diff --git a/isar/isar.el b/isar/isar.el
index d5d13c04..34949e3a 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -383,6 +383,8 @@ proof-shell-retract-files-regexp."
["inner syntax" isar-help-syntax t]
["methods" isar-help-methods t])))))
+(defalias 'isar-set-command 'isa-set-isabelle-command)
+
(defpgdefault help-menu-entries isabelle-docs-menu)
;; undo proof commands