Make proof-shell-quit-timeout a prover-specific customize option, default to 45 for Isar. See http://proofgeneral.inf.ed.ac.uk/trac/ticket/384.

3 files changed, 18 insertions, 14 deletions

diff --git a/generic/pg-custom.el b/generic/pg-custom.el
index 5218cda5..5122416e 100644
--- a/generic/pg-custom.el
+++ b/generic/pg-custom.el
@@ -11,7 +11,7 @@
 ;; Prover specific settings and user options.
 ;;
 ;; The settings defined here automatically use the current proof
-;; assistant symbol as a prefix, i.e.  isa-favourites, coq-favourites,
+;; assistant symbol as a prefix, i.e.  isar-favourites, coq-favourites,
 ;; or whatever will be defined on evaluation.
 ;;
 ;; This file is loaded only by mode stubs defined in `proof-site.el',
@@ -108,6 +108,18 @@ For example for coq on Windows you might need something like:
   :type '(list string)
   :group 'proof-shell)
 
+(defpgcustom quit-timeout 
+  (cond
+   ((eq proof-assistant-symbol 'isar)    45)
+   (t					 5))
+  "The number of seconds to wait after sending `proof-shell-quit-cmd'.
+After this timeout, the proof shell will be killed off more rudely.
+If your proof assistant takes a long time to clean up (for
+example writing persistent databases out or the like), you may
+need to bump up this value."
+   :type 'number
+   :group 'proof-shell)
+
 (defpgcustom favourites nil
   "*Favourite commands for this proof assistant.
 A list of lists of the form (COMMAND INSCRIPT MENUNAME KEY),
diff --git a/generic/proof-config.el b/generic/proof-config.el
index 926cb024..8ce2c86c 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -811,9 +811,10 @@ See pg-user.el: `pg-create-in-span-context-menu' for more hints."
 
 (defcustom proof-prog-name nil
   "System command to run the proof assistant in the proof shell.
-May contain arguments separated by spaces, but see also `proof-prog-args'.
+May contain arguments separated by spaces, but see also the
+prover specific settings `<PA>-prog-args' and `<PA>-prog-env'.
 
-Remark: if `proof-prog-args' is non-nil, then `proof-prog-name' is considered
+Remark: if `<PA>-prog-args' is non-nil, then `proof-prog-name' is considered
 strictly: it must contain *only* the program name with no option, spaces
 are interpreted literally as part of the program name."
   :type 'string
@@ -870,15 +871,6 @@ See also `proof-shell-pre-sync-init-cmd'."
    :type '(choice string (const nil))
    :group 'proof-shell)
 
-(defcustom proof-shell-quit-timeout 5
-  "The number of seconds to wait after sending `proof-shell-quit-cmd'.
-After this timeout, the proof shell will be killed off more rudely.
-If your proof assistant takes a long time to clean up (for
-example writing persistent databases out or the like), you may
-need to bump up this value."
-   :type '(choice string (const nil))
-   :group 'proof-shell)
-
 (defcustom proof-shell-cd-cmd nil
   "Command to the proof assistant to change the working directory.
 The format character `%s' is replaced with the directory, and
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 5c757cc6..2832c6c2 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -412,14 +412,14 @@ shell buffer, alled by `proof-shell-bail-out' if process exits."
 	
 	;; Turn off scripting (ensure buffers completely processed/undone)
 	(proof-deactivate-scripting-auto)
-	(proof-shell-wait proof-shell-quit-timeout)
+	(proof-shell-wait (proof-ass quit-timeout))
 	
 	;; Try to shut down politely.  
 	(if proof-shell-quit-cmd
 	    (scomint-send-string proc
 				 (concat proof-shell-quit-cmd "\n"))
 	  (scomint-send-eof))
-	(proof-shell-wait nil proof-shell-quit-timeout)
+	(proof-shell-wait nil (proof-ass quit-timeout))
 	
 	;; Still there, kill it rudely.
 	(when (memq (process-status proc) '(open run stop))