Added proof-mode-for-script setting.

4 files changed, 16 insertions, 7 deletions

diff --git a/coq/coq.el b/coq/coq.el
index c4390a9a..4e4a173f 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -329,6 +329,8 @@
 
   (setq proof-www-home-page coq-www-home-page)
 
+  (setq proof-mode-for-script 'coq-mode)
+
   (setq proof-prf-string "Show"
 	proof-ctxt-string "Print All"
 	proof-help-string "Help")
diff --git a/generic/proof-config.el b/generic/proof-config.el
index 676f317d..a62292b1 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -196,24 +196,25 @@ from the name given in proof-internal-assistant-table."
 (defcustom proof-mode-for-shell nil
   "Mode for proof shell buffers.
 Suggestion: this can be set in proof-pre-shell-start-hook."
-  :type 'function
+  :type 'symbol
   :group 'prover-config)
 
 (defcustom proof-mode-for-pbp nil
   "Mode for proof state display buffers.
 Suggestion: this can be set in proof-pre-shell-start-hook."
-  :type 'function
+  :type 'symbol
   :group 'prover-config)
 
 (defcustom proof-mode-for-script nil
-  "Major mode for proof script buffers."
-  :type 'function
+  "Mode for proof script buffers.
+This is used by Proof General to find out which buffers 
+contain proof scripts.
+Suggestion: this can be set in the script mode configuration."
+  :type 'symbol
   :group 'prover-config)
 
 
 
-
-
 
 ;;
 ;; 3. Configuration for menus, user-level commands, etc.
@@ -443,7 +444,10 @@ assistant, for example, to switch to a new theory."
 
 (defcustom proof-prog-name nil
   "System command to run program name in proof shell.
-Suggestion: this can be set in proof-pre-shell-start-hook."
+Suggestion: this can be set in proof-pre-shell-start-hook from
+a variable which is in the proof assistant's customization
+group.  This allows different proof assistants to coexist
+(albeit in separate Emacs sessions)."
   :type 'string
   :group 'proof-shell)
 
diff --git a/isa/isa.el b/isa/isa.el
index 41ffcd2d..03413ad0 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -53,6 +53,7 @@ no regular or easily discernable structure."
   "Configure generic proof scripting mode variables for Isabelle."
   (setq
    proof-www-home-page		isabelle-web-page
+   proof-mode-for-script	'isa-proofscript-mode
    ;; proof script syntax
    proof-terminal-char		?\;	; ends a proof
    proof-comment-start		"(*"	; comment in a proof
diff --git a/lego/lego.el b/lego/lego.el
index a35d28bf..f0564857 100644
--- a/lego/lego.el
+++ b/lego/lego.el
@@ -378,6 +378,8 @@
 
   (setq proof-www-home-page lego-www-home-page)
 
+  (setq proof-mode-for-script 'lego-mode)
+
   (setq proof-prf-string "Prf"
 	proof-goal-command "Goal %s;"
 	proof-save-command "Save %s;"