From 6705f896cb0fffceaab3d7b4cdb2921a70e769a2 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Tue, 25 Aug 2009 11:51:02 +0000
Subject: Add menu entry for setting proof assistant command

---
 generic/proof-menu.el | 7 ++++++-
 isar/isar.el          | 2 ++
 2 files changed, 8 insertions(+), 1 deletion(-)

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
-- 
cgit v1.2.3