Reimplemented functions to shut down and restart proof process.

Scrapped proof-shell-exit-hook.
Added proof-shell-quit-cmdd, proof-shell-restart-comd
Fancier Scripting indicator for active scripting buffer.

5 files changed, 192 insertions, 127 deletions

diff --git a/generic/proof-config.el b/generic/proof-config.el
index e70a8963..4a5fee18 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -616,6 +616,16 @@ group.  This allows different proof assistants to coexist
    :type '(choice string (const nil))
    :group 'proof-shell)
 
+(defcustom proof-shell-restart-cmd ""
+   "A command for re-initialising the proof process."
+   :type '(choice string (const nil))
+   :group 'proof-shell)
+
+(defcustom proof-shell-quit-cmd ""
+  "A command to quit the proof process.  If nil, send EOF instead."
+   :type '(choice string (const nil))
+   :group 'proof-shell)
+
 (defcustom proof-shell-cd nil
   "Command to the proof assistant to change the working directory."
   :type 'string
@@ -816,6 +826,7 @@ data triggered by `proof-shell-retract-files-regexp'."
 
 
 
+
 
 ;;
 ;; 6. Global constants
diff --git a/generic/proof-script.el b/generic/proof-script.el
index ba4c3898..5e4f6f69 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -132,7 +132,10 @@ proof-script-next-entity-regexps, which see."
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 (deflocal proof-locked-span nil
-  "The locked span of the buffer.")
+  "The locked span of the buffer.
+Each script buffer has its own locked span, which may be detached.
+Proof General allows buffers in other modes also to be locked;
+these also have span regions.")
 
 ;; FIXME da: really we only need one queue span rather than one per
 ;; buffer, but I've made it local because the initialisation occurs in
@@ -376,7 +379,7 @@ If non-nil, point is left where it was."
   (not (re-search-backward "\\S-" (proof-unprocessed-begin) t)))
 
 (defun proof-activate-scripting ()
-  "Activate scripting minor mode for current scripting buffer. 
+  "Activate scripting minor mode for current scripting buffer.
 
 The current buffer is prepared for scripting.  No changes are
 necessary if it is already in Scripting minor mode. Otherwise, it
@@ -440,6 +443,7 @@ the hooks `proof-activate-scripting-hook' are run."
 
     ;; This may be a good time to ask if the user wants to save some
     ;; buffers
+    ;; FIXME: no, move it elsewhere.
     (save-some-buffers))))
 
 
@@ -1110,38 +1114,38 @@ the proof script."
   (goto-char (point-max))
   (proof-assert-until-point))
 
-(defun proof-restart-buffer (buffer)
-  "Remove all extents in BUFFER and maybe reset `proof-script-buffer'.
-No effect if BUFFER is nil or killed.  
-If BUFFER is current scripting buffer, then proof-script-buffer 
-will be reset."
-  (save-excursion
-    (if (buffer-live-p buffer)
-	(with-current-buffer buffer
-	  (if proof-active-buffer-fake-minor-mode
-	      (setq proof-active-buffer-fake-minor-mode nil))
-	  (delete-spans (point-min) (point-max) 'type)
-	  (proof-detach-segments)))
-    (if (eq buffer proof-script-buffer)
-	(setq proof-script-buffer nil))))
-
-(defun proof-restart-buffers (bufferlist)
-  "Remove all spans in BUFFERLIST and update `proof-script-buffer'."
-  (mapcar 'proof-restart-buffer bufferlist))
-
-(defun proof-scripting-buffers ()
-  "Return a list of all script buffers, i.e. those in proof-mode-for-script."
-  (proof-buffers-in-mode proof-mode-for-script))
-
-(defun proof-restart-all-buffers ()
-  "Remove all spans in from scripting buffers and included files."
-  ;; Do both script buffers and included files list because
-  ;; we allow non-script buffers to be locked also.
-  (proof-restart-buffers
-   (mapcar 'proof-file-to-buffer proof-included-files-list))
-  (proof-restart-bufers
-   (proof-buffers-in-mode proof-mode-for-script)))
-  
+(defun proof-restart-buffers (buffers)
+  "Remove all extents in BUFFERS and maybe reset `proof-script-buffer'.
+No effect on a buffer which is nil or killed.  If one of the buffers
+is the current scripting buffer, then proof-script-buffer 
+will deactivated."
+  (mapcar
+   (lambda (buffer)
+     (save-excursion
+       (if (buffer-live-p buffer)
+	   (with-current-buffer buffer
+	     (if proof-active-buffer-fake-minor-mode
+		 (setq proof-active-buffer-fake-minor-mode nil))
+	     (delete-spans (point-min) (point-max) 'type)
+	     (proof-detach-segments buffer)))
+       (if (eq buffer proof-script-buffer)
+	   (setq proof-script-buffer nil))))
+   buffers))
+
+(defun proof-script-buffers-with-spans ()
+  "Return a list of all buffers with spans.
+This is calculated by finding all the buffers with a non-nil
+value of proof-locked span."
+  (let ((bufs-left (buffer-list)) 
+	bufs-got)
+    (dolist (buf bufs-left bufs-got)
+      (if (with-current-buffer buf proof-locked-span)
+	  (setq bufs-got (cons buf bufs-got))))))
+
+(defun proof-script-remove-all-spans-and-deactivate ()
+  "Remove all spans from scripting buffers via proof-restart-buffers."
+  (proof-restart-buffers (proof-script-buffers-with-spans)))
+
 ;; For when things go horribly wrong
 ;; FIXME: this needs to politely stop the process by sending
 ;; an EOF or customizable command.  (maybe timeout waiting for
@@ -1150,34 +1154,24 @@ will be reset."
 ;;  Put a funciton to remove all extents in buffers into
 ;; the kill-buffer-hook for the proof shell.  Then this
 ;; function just stops the shell nicely (see proof-stop-shell).
-(defun proof-restart-script ()
-  "Restart Proof General.
-Kill off the proof assistant process and remove all markings in the
-script buffers."
-  (interactive)
-  (proof-restart-all-buffers)
-  (setq proof-included-files-nil
-	proof-shell-busy nil
-	proof-shell-proof-completed nil)
-  (if (buffer-live-p proof-shell-buffer) 
-      (kill-buffer proof-shell-buffer))
-  (if (buffer-live-p proof-pbp-buffer)
-      (kill-buffer proof-pbp-buffer))
-  (and (buffer-live-p proof-response-buffer)
-       (kill-buffer proof-response-buffer)))
-
-;; For when things go not-quite-so-horribly wrong
-;; FIXME: this may need work, and maybe isn't needed at
-;; all (proof-retract-file when it appears may be enough).
-(defun proof-restart-script-same-process ()
-  (interactive)
-  (save-excursion
-    (if (buffer-live-p proof-script-buffer)
-	(progn
-	  (set-buffer proof-script-buffer)
-	  (setq proof-active-buffer-fake-minor-mode nil)
-	  (delete-spans (point-min) (point-max) 'type)
-	  (proof-detach-segments)))))
+
+;(defun proof-restart-script ()
+;  "Restart Proof General.
+;Re-initialise the proof assistant by sending the restart command,
+;and clear all locked regions."
+;  (interactive)
+;  (proof-script-remove-all-spans-and-deactivate)
+;  (setq proof-included-files nil
+;	proof-shell-busy nil
+;	proof-shell-proof-completed nil)
+;  (if (buffer-live-p proof-shell-buffer) 
+;      (kill-buffer proof-shell-buffer))
+;  (if (buffer-live-p proof-pbp-buffer)
+;      (kill-buffer proof-pbp-buffer))
+;  (and (buffer-live-p proof-response-buffer)
+;       (kill-buffer proof-response-buffer)))
+
+
 
 ;; A command for making things go horribly wrong - it moves the
 ;; end-of-locked-region marker backwards, so user had better move it
@@ -1344,12 +1338,6 @@ Start up the proof assistant if necessary."
 
 
 
-;;; To be called from menu
-(defun proof-menu-invoke-info ()
-  "Call info on Proof General."
-  (interactive)
-  (info "ProofGeneral"))
-
 ;; A handy utility function used in buffer menu.
 (defun proof-switch-to-buffer (buf &optional noselect)
   "Switch to or display buffer BUF in other window unless already displayed.
@@ -1363,18 +1351,14 @@ No action if BUF is nil."
 	     (display-buffer buf t)
 	   (switch-to-buffer-other-window buf)))))
 
-(defun proof-menu-exit ()
-  "Exit Proof-assistant."
-  (interactive)
-  (proof-restart-script))
-
 (defvar proof-help-menu
   `("Help"
     [,(concat proof-assistant " web page")
      (browse-url proof-assistant-home-page) t]
     ["Proof General home page"
      (browse-url proof-proof-general-home-page) t]
-    ["Proof General Info" proof-menu-invoke-info t]
+    ["Proof General Info"
+     (info "Proof General") t]
     )
   "Proof General help menu.")
 
@@ -1397,11 +1381,17 @@ No action if BUF is nil."
 (defvar proof-shared-menu
   (append
     (list
-     ["Display context" proof-ctxt
+     ["Display context"
+      proof-ctxt
+      :active (proof-shell-live-buffer)]
+     ["Display proof state"
+      proof-prf
       :active (proof-shell-live-buffer)]
-     ["Display proof state" proof-prf
+     ["Restart"
+      proof-shell-restart
       :active (proof-shell-live-buffer)]
-     ["Exit proof assistant" proof-menu-exit
+     ["Exit proof assistant"
+      proof-shell-exit
       :active (proof-shell-live-buffer)])
     (list proof-help-menu)
     (list proof-buffer-menu))
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 6a9a85de..1216e337 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -169,9 +169,10 @@ No error messages.  Useful as menu or toolbar enabler."
   (setq proof-shell-busy nil))
 
 
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;  Starting and stopping the proof-system shell                    ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+;;
+;;  Starting and stopping the proof shell  
+;;
 
 (defun proof-start-shell ()
   "Initialise a shell-like buffer for a proof assistant.
@@ -186,6 +187,9 @@ Does nothing if proof assistant is already running."
 	(save-excursion
 	  (setq proof-prog-name (read-shell-command "Run process: "
 						    proof-prog-name))))
+    ;; FIXME da: why do we need this?  We never have more than
+    ;; one proof shell running at a time.  We might as well
+    ;; kill off the old buffer anyway.
     (let ((proc
 	   (concat "Inferior "
 		   (substring proof-prog-name
@@ -212,57 +216,114 @@ Does nothing if proof assistant is already running."
 	      " ")))
 	(apply 'make-comint  (append (list proc (car prog-name-list) nil)
 				     (cdr prog-name-list))))
-      ;; To send any initialisation commands to the inferior process,
-      ;; consult proof-shell-config-done...
-
+      
+      ;; Create the associated buffers and set buffer variables
       (setq proof-shell-buffer (get-buffer (concat "*" proc "*"))
 	    proof-pbp-buffer (get-buffer-create (concat "*" proc "-goals*"))
 	    proof-response-buffer (get-buffer-create (concat "*" proc
 	    "-response*")))
-
       (save-excursion
 	(set-buffer proof-shell-buffer)
+	(make-variable-buffer-local 'kill-buffer-hook)
+	(add-hook 'kill-buffer-hook 'proof-shell-kill-function t)
 	(funcall proof-mode-for-shell)
 	(set-buffer proof-response-buffer)
 	(funcall proof-mode-for-response)
 	(set-buffer proof-pbp-buffer)
 	(funcall proof-mode-for-pbp))
 
-      ;; FIXME: Maybe this belongs outside this function?
-      (or (assq 'proof-active-buffer-fake-minor-mode minor-mode-alist)
-	  (setq minor-mode-alist
-		(append minor-mode-alist
-			(list '(proof-active-buffer-fake-minor-mode 
-				" Scripting")))))
-
       (message 
        (format "Starting %s process... done." proc)))))
-  
 
-;; Should this be the same as proof-restart-script?
-;; Perhaps this is redundant.
-(defun proof-stop-shell ()
-  "Exit the proof process.  Runs proof-shell-exit-hook if non-nil"
+
+;;
+;; Indicator and fake minor mode for active scripting buffer
+;; 
+
+(defcustom proof-shell-active-scripting-indicator
+  (if (string-match "XEmacs" emacs-version)
+      (cons (make-extent nil nil) " Scripting ")
+    "Scripting")
+  "Modeline indicator for active scripting buffer.
+If first component is extent it will automatically follow the colour
+of the queue region."
+  :type 'sexp
+  :group 'proof-general-internals)
+
+(cond
+ ((string-match "XEmacs" emacs-version)
+  (if (extentp (car proof-shell-active-scripting-indicator))
+      (set-extent-properties
+       (car proof-shell-active-scripting-indicator)
+       '(face proof-locked-face)))))
+
+(setq minor-mode-alist
+      (append minor-mode-alist
+	      (list '(proof-active-buffer-fake-minor-mode
+		      proof-shell-active-scripting-indicator))))
+
+
+
+;;
+;;  Shutting down proof shell and associated buffers
+;;
+
+(defun proof-shell-kill-function ()
+  "Function run when a proof-shell buffer is killed.
+Value for kill-buffer-hook in shell buffer.
+It shuts down the proof process nicely and clears up all locked regions
+and state variables."
+  (let ((alive    (comint-check-proc (current-buffer)))
+	(proc     (get-buffer-process (current-buffer)))
+	(procname (and proc (process-name proc))))
+	
+    (if alive				; process still there
+	(progn
+	  (mesage "%s exiting..." procname)
+	  ;; Try to shut it down politely
+	  (if proof-shell-quit-cmd
+	      (comint-send-string proof-shell-quit-cmd)
+	    (comint-send-eof))
+	  ;; Wait a while for it to die
+	  (while (> 1 (process-exit-status proc))
+	    (accept-process-output proc 15))))
+    ;; Restart all scripting buffers
+    (proof-script-remove-all-spans-and-deactivate)
+    ;; Clear state
+    (setq proof-included-files-list nil
+	  proof-shell-busy nil
+	  proof-shell-proof-completed nil)
+    ;; Kill buffers associated with shell buffer
+    (if (buffer-live-p proof-pbp-buffer)
+	(kill-buffer proof-pbp-buffer))
+    (if (buffer-live-p proof-response-buffer)
+	(kill-buffer proof-response-buffer))
+    (message "%s terminated." procname)))
+
+(defun proof-shell-exit ()
+  "Query the user and exit the proof process.
+This simply kills the proof-shell-buffer relying on the hook function
+to do the hard work."
   (interactive)
-  (save-excursion
-    (let ((buffer (proof-shell-live-buffer)) 
-	  proc)
-      (if buffer
-	  (progn
-	    (save-excursion
-	      (set-buffer buffer)
-	      (setq proc (process-name (get-buffer-process)))
-	      (comint-send-eof)
-	      (proof-restart-all-buffers)
-	      (kill-buffer))
-	    (run-hooks 'proof-shell-exit-hook)
-
-             ;;it is important that the hooks are
-	     ;;run after the buffer has been killed. In the reverse
-	     ;;order e.g., intall-shell-fonts causes problems and it
-	     ;;is impossible to restart the PROOF shell
-
-	    (message (format "%s process terminated." proc)))))))
+  (if (buffer-live-p proof-shell-buffer)
+      (if (yes-or-no-p (format "Exit %s process? " proof-assistant))
+	  (kill-buffer proof-shell-buffer)
+	(error "No proof shell buffer to kill!"))))
+
+(defun proof-shell-restart ()
+  "Restart the proof shell by sending the restart command
+and clearing all script buffers."
+  (interactive)
+  (proof-script-remove-all-spans-and-deactivate)
+  (setq proof-included-files-list nil
+	proof-shell-busy nil
+	proof-shell-proof-completed nil)
+  (if (and (buffer-live-p proof-shell-buffer)
+	   proof-shell-restart-cmd)
+	   (proof-shell-invisible-command
+	    proof-shell-restart-cmd)))
+
+
 
 
 
@@ -353,12 +414,13 @@ Does nothing if proof assistant is already running."
 (defvar proof-shell-erase-response-flag nil
   "Indicates that the response buffer should be cleared before next message.")
 
-(defun proof-shell-maybe-erase-response (&optional erase-next-time
-						   clean-windows)
+(defun proof-shell-maybe-erase-response
+  (&optional erase-next-time clean-windows force)
   "Erase the response buffer according to proof-shell-erase-response-flag.
 ERASE-NEXT-TIME is the new value for the flag.
-If CLEAN-WINDOWS is set, use proof-clear-buffer to do the erasing."
-  (if proof-shell-erase-response-flag
+If CLEAN-WINDOWS is set, use proof-clear-buffer to do the erasing.
+If FORCE, override proof-shell-erase-response-flag."
+  (if (or proof-shell-erase-response-flag force)
       (if clean-windows
 	  (proof-clean-buffer proof-response-buffer)
 	(erase-buffer proof-response-buffer)))
@@ -939,7 +1001,7 @@ if none of these apply, display."
 	 (string-match proof-shell-clear-response-regexp message)
 	 proof-response-buffer)
     ;; Erase response buffer and possibly its windows.
-    (proof-shell-maybe-erase-response nil t))
+    (proof-shell-maybe-erase-response nil t t))
 
    (t
     ;; We're about to display a message.  Clear the response buffer
@@ -1199,11 +1261,13 @@ Annotations are characters 128-255."
     ;; to adjust the directory. Perhaps one might even want to issue
     ;; this command whenever a new scripting buffer is active?
     (and proof-shell-cd
-	 (proof-shell-insert (format proof-shell-cd
-				     ;; under Emacs 19.34 default-directory contains "~" which causes
-				     ;; problems with LEGO's internal Cd command
-				     (expand-file-name default-directory))))
-
+	 (proof-shell-insert
+	  (format proof-shell-cd
+		  ;; under Emacs 19.34 default-directory contains "~"
+		  ;; which causes problems with LEGO's internal Cd
+		  ;; command
+		  (expand-file-name default-directory))))
+    
     (if proof-shell-init-cmd
 	(proof-shell-insert proof-shell-init-cmd))
 
diff --git a/generic/proof-toolbar.el b/generic/proof-toolbar.el
index 1e2cc44f..44c37a9e 100644
--- a/generic/proof-toolbar.el
+++ b/generic/proof-toolbar.el
@@ -355,8 +355,7 @@ Move point if the end of the locked position is invisible."
 (defun proof-toolbar-restart  ()
   (interactive)
   (if (proof-toolbar-restart-enable-p)
-      (if (yes-or-no-p (concat "Restart " proof-assistant " scripting?"))
-	   (proof-restart-script))))
+      (proof-shell-restart)))
 
 ;;
 ;; Goal button
diff --git a/generic/proof.el b/generic/proof.el
index 64f57d1e..5a7c6d9b 100644
--- a/generic/proof.el
+++ b/generic/proof.el
@@ -186,6 +186,7 @@ frame is the one showing the script buffer.)"
       (delete-windows-on buffer t)))
 
 ;; utility function
+;; FIXME da: maybe not used.  Put into spare parts file.
 (defun proof-buffers-in-mode (mode &optional buflist)
   "Return a list of the buffers in the buffer list in major-mode MODE.
 Restrict to BUFLIST if it's set."