From e5c96b5a60eec1a64de3fd93d0d21e867a09c0f5 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Fri, 23 Oct 1998 10:02:31 +0000 Subject: Added proof-mode-for-script setting. --- generic/proof-config.el | 18 +++++++++++------- 1 file changed, 11 insertions(+), 7 deletions(-) (limited to 'generic/proof-config.el') 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) -- cgit v1.2.3