proof-check-process-available replaced by *two* functions:

 proof-activate-scripting
 proof-shell-ready-prover

3 files changed, 244 insertions, 158 deletions

diff --git a/generic/proof-script.el b/generic/proof-script.el
index 967d3073..99764e40 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -19,17 +19,10 @@
 ;; commands need to have the terminal string, some don't.
 ;; We should assume commands are terminated properly at the
 ;; specific level.
+
 (defvar proof-terminal-string nil 
   "End-of-line string for proof process.")
 
-(defvar proof-re-end-of-cmd nil 
-  "Regexp matching end of command.  Based on proof-terminal-string.
-Set in proof-config-done.")
-
-(defvar proof-re-term-or-comment nil 
-  "Regexp matching terminator, comment start, or comment end.
-Set in proof-config-done.")
-
 (defvar proof-marker nil 
   "Marker in proof shell buffer pointing to previous command input.")
 
@@ -48,11 +41,6 @@ The cdr of the list of corresponding file names is a subset of
 (defvar proof-response-buffer nil
   "The response buffer.")
 
-(defvar proof-shell-busy nil 
-  "A lock indicating that the proof shell is processing.
-When this is non-nil, proof-check-process-available will give
-an error.")
-
 (deflocal proof-buffer-type nil 
   "Symbol indicating the type of this buffer: 'script, 'shell, or 'pbp.")
 
@@ -317,10 +305,15 @@ to allow other files loaded by proof assistants to be marked read-only."
 	(progn
 	  (setq proof-included-files-list
 		(cons cfile proof-included-files-list))
-	  (or (equal cfile
-		     (file-truename (buffer-file-name
-				     (car proof-script-buffer-list))))
-	      (not buffer)
+	  ;; If the file is loaded into a buffer, which isn't
+	  ;; the current scripting buffer, then put an
+	  ;; atomic locked region in it.
+	  (if (and buffer
+		   proof-script-buffer-list
+		   (not (equal cfile
+			       (file-truename 
+				(buffer-file-name
+				 (car proof-script-buffer-list))))))
 	      (proof-mark-buffer-atomic buffer))))))
 
 ;; three NEW predicates, let's use them!
@@ -344,74 +337,67 @@ NB: If nil, point is left at first non-whitespace character found.
 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. 
 
-(defun proof-check-process-available (&optional relaxed)
-  "Adjust internal variables for scripting of current buffer.
-
-Makes sure there is a proof shell running and that it isn't
-busy.  If it is busy, an error is signaled.
-
-If RELAXED is non-nil, nothing more is done. 
-
-Otherwise, the current buffer is prepared for scripting.  No changes
-are necessary if it is already in Scripting minor mode. Otherwise, the
-it will become the current scripting buffer provided the current
+The current buffer is prepared for scripting.  No changes are
+necessary if it is already in Scripting minor mode. Otherwise, it
+will become the current scripting buffer provided the current
 scripting buffer has either no locked region or everything in it has
-been processed."
-  (proof-start-shell)
-  (cond
-   ((not (or relaxed (eq proof-buffer-type 'script)))
-    (error "Must be running in a script buffer"))
-   (proof-shell-busy (error "Proof Process Busy!"))
-   (relaxed ())			;exit cond
+been processed.
 
-   ;; No buffer is in Scripting minor mode.
-   ;; We assume the setup is done somewhere else
-   ;; so this should never happen
-   ((null proof-script-buffer-list) (assert nil))
+When a new script buffer has scripting minor mode turned on,
+the hooks `proof-activate-scripting-hook' are run."
+  (cond 
+   ((not (eq proof-buffer-type 'script)) 
+    (error "Must be running in a script buffer"))
 
-   ;; The current buffer is in Scripting minor mode
-   ;; so there's nothing to do
-   ((equal (current-buffer) (car proof-script-buffer-list)))
+   ;; If the current buffer is the active one there's nothing to do.
+   ((equal (current-buffer) (car-safe proof-script-buffer-list)))
 
+   ;; Otherwise we need to activate a new Scripting buffer.
    (t
-    (let ((script-buffer (car proof-script-buffer-list))
-	  (current-buffer (current-buffer)))
-      (save-excursion
-	(set-buffer script-buffer)
-	;; We only allow switching of the Scripting buffer if the
-	;; locked region is either empty or full for all buffers.
-	;; Here we check the current Scripting buffer's status.
-	(if (proof-locked-region-full-p)
-	    ;; We're switching from a buffer which has been
-	    ;; completely processed.  Make sure that it's
-	    ;; registered on the included files list, in
-	    ;; case it has been processed piecemeal.
-	    (if buffer-file-name
-		(proof-register-possibly-new-processed-file 
-		 buffer-file-name)))
-
-	(if (or 
-	     (proof-locked-region-empty-p)
-	     (proof-locked-region-full-p))
-	    ;; we are changing the scripting buffer
-	    (progn
-	      (setq proof-active-buffer-fake-minor-mode nil)
-	      (set-buffer current-buffer)
-	      
-	      ;; does the current buffer contain locked regions already?
-	      (if (member current-buffer proof-script-buffer-list)
-		  (setq proof-script-buffer-list
-			(remove current-buffer proof-script-buffer-list))
-		(proof-init-segmentation))
-	      (setq proof-script-buffer-list
-		    (cons current-buffer proof-script-buffer-list))
-	      (setq proof-active-buffer-fake-minor-mode t)
-	      (run-hooks 'proof-activate-scripting-hook))
-	  ;; Locked region covers only part of the buffer
-	  ;; FIXME da: ponder alternative of trying to complete rest
-	  ;; of current scripting buffer?
-	  (error "Cannot deal with two unfinished script buffers!")))))))
+    (if proof-script-buffer-list
+	(save-excursion
+	  ;; We're switching from another scripting buffer
+	  ;; to a new one.  Examine the old buffer.
+	  (set-buffer (car proof-script-buffer-list))
+	    
+	  ;; We only allow switching of the Scripting buffer if the
+	  ;; locked region is either empty or full for all buffers.
+	  (or (proof-locked-region-empty-p)
+	      (proof-locked-region-full)
+	      (error 
+	       ;; FIXME da: ponder alternative of trying to complete rest
+	       ;; of current scripting buffer?
+	       "Cannot deal with two unfinished script buffers!"))
+	    
+	  (if (proof-locked-region-full-p)
+	      ;; We're switching from a buffer which has been
+	      ;; completely processed.  Make sure that it's
+	      ;; registered on the included files list. 
+	      (if buffer-file-name
+		  (proof-register-possibly-new-processed-file 
+		   buffer-file-name)))
+
+	  ;; Turn off Scripting in the old buffer.
+	  (setq proof-active-buffer-fake-minor-mode nil)))
+
+    ;; is this a fresh script mode buffer, with no locked region?
+    (if (not (member (current-buffer) proof-script-buffer-list))
+	(progn
+	  (proof-init-segmentation)
+	  (setq proof-script-buffer-list
+		(cons (current-buffer) proof-script-buffer-list))))
+
+    ;; Turn on the minor mode, run hooks.
+    (setq proof-active-buffer-fake-minor-mode t)
+    (run-hooks 'proof-activate-scripting-hook)
+
+    ;; Make status of active scripting buffer show up
+    (if (fboundp 'redraw-modeline)
+	(redraw-modeline)
+      (force-mode-line-update)))))
 
 
 
@@ -751,9 +737,10 @@ the comment. If you want something different, put it inside
 unclosed-comment-fun. If ignore-proof-process-p is set, no commands
 will be added to the queue."
   (interactive)
-  (let ((pt (point))
-	(crowbar (or ignore-proof-process-p (proof-check-process-available)))
-	semis)
+  (or ignore-proof-process-p 
+      (proof-shell-ready-prover))
+  (proof-activate-scripting)
+  (let ((semis))
     (save-excursion
       ;; Give error if no non-whitespace between point and end of locked region.
       (if (proof-only-whitespace-to-locked-region-p)
@@ -763,12 +750,11 @@ will be added to the queue."
     (if (and unclosed-comment-fun (eq 'unclosed-comment (car semis)))
 	(funcall unclosed-comment-fun)
       (if (eq 'unclosed-comment (car semis)) (setq semis (cdr semis)))
-      (if (and (not ignore-proof-process-p) (not crowbar) (null semis))
+      (if (and (not ignore-proof-process-p) (null semis))
 	  (error "I don't know what I should be doing in this buffer!"))
       (goto-char (nth 2 (car semis)))
       (and (not ignore-proof-process-p)
 	   (let ((vanillas (proof-semis-to-vanillas (nreverse semis))))
-;	     (if crowbar (setq vanillas (cons crowbar vanillas)))
 	     (proof-start-queue (proof-unprocessed-begin) (point) vanillas))))))
 
 
@@ -797,11 +783,13 @@ Afterwards, move forward to near the next command afterwards, unless
 DONT-MOVE-FORWARD is non-nil.  If FOR-NEW-COMMAND is non-nil,
 a space or newline will be inserted automatically."
   (interactive)
-  (let ((pt (point))
-	(crowbar (or ignore-proof-process-p (proof-check-process-available)))
-	semis)
-    (if (proof-locked-region-full-p)
-	(error "Locked region is full, no more commands to do!"))
+  (or ignore-proof-process-p 
+      (proof-shell-ready-prover))
+  (proof-activate-scripting)
+  (or ignore-proof-process-p
+      (if (proof-locked-region-full-p)
+	  (error "Locked region is full, no more commands to do!")))
+  (let ((semis))
     (save-excursion
       ;; CHANGE from old proof-assert-until-point: don't bother check
       ;; for non-whitespace between locked region and point.
@@ -817,7 +805,7 @@ a space or newline will be inserted automatically."
 	(funcall unclosed-comment-fun)
       (if (eq 'unclosed-comment (car-safe semis))
 	  (setq semis (cdr semis)))
-      (if (and (not ignore-proof-process-p) (not crowbar) (null semis))
+      (if (and (not ignore-proof-process-p) (null semis))
 	  (error "I don't know what I should be doing in this buffer!"))
       (goto-char (nth 2 (car semis)))
       (if (not ignore-proof-process-p)
@@ -837,7 +825,8 @@ a space or newline will be inserted automatically."
 ;;         command for us to run                                    ;;
 
 (defun proof-insert-pbp-command (cmd)
-  (proof-check-process-available)
+  (proof-shell-ready-prover)			; FIXME
+  (proof-activate-scripting)
   (let (span)
     (proof-goto-end-of-locked)
     (insert cmd)
@@ -918,7 +907,8 @@ deletes the region corresponding to the proof sequence."
    this function is invoked outside a locked region, the last
    successfully processed command is undone."
   (interactive)
-  (proof-check-process-available)
+  (proof-shell-ready-prover)
+  (proof-activate-scripting)
   (let ((span (span-at (point) 'type)))
     (if (null (proof-locked-end)) (error "No locked region"))
     (and (null span)
@@ -934,22 +924,21 @@ deletes the region corresponding to the proof sequence."
 ;;         something here which changes the proof state             ;;
 
 (defun proof-done-trying (span)
+  "Callback for proof-try-command."
   (delete-span span)
   (proof-detach-queue))
 			
-(defun proof-try-command
-  (&optional unclosed-comment-fun) 
-
-  "Process the command at point,
-   but don't add it to the locked region. This will only happen if
-   the command satisfies proof-state-preserving-p.
+(defun proof-try-command (&optional unclosed-comment-fun) 
+  "Process the command at point, but don't add it to the locked region. 
+This will only happen if the command satisfies proof-state-preserving-p.
 
-   Default action if inside a comment is just to go until the start of
-   the comment. If you want something different, put it inside
-   unclosed-comment-fun."
+Default action if inside a comment is just to go until the start of
+the comment. If you want something different, put it inside
+unclosed-comment-fun."
   (interactive)
-  (let ((pt (point)) semis crowbar test)
-    (setq crowbar (proof-check-process-available))
+  (proof-shell-ready-prover)
+  (proof-activate-scripting)
+  (let ((pt (point)) semis test)
     (save-excursion
       (if (proof-only-whitespace-to-locked-region-p)
 	  (progn (goto-char pt)
@@ -958,14 +947,14 @@ deletes the region corresponding to the proof sequence."
     (if (and unclosed-comment-fun (eq 'unclosed-comment (car semis)))
 	(funcall unclosed-comment-fun)
       (if (eq 'unclosed-comment (car semis)) (setq semis (cdr semis)))
-      (if (and (not crowbar) (null semis)) (error "I don't know what I should be doing in this buffer!"))
+      (if (null semis) 
+	  (error "I don't know what I should be doing in this buffer!"))
       (setq test (car semis))
       (if (not (funcall proof-state-preserving-p (nth 1 test)))
-	  (error "Command is not state preserving"))
+	  (error "Command is not state preserving, I won't try it."))
       (goto-char (nth 2 test))
       (let ((vanillas (proof-semis-to-vanillas (list test)
 					       'proof-done-trying)))
-;	(if crowbar (setq vanillas (cons crowbar vanillas)))
 	(proof-start-queue (proof-unprocessed-begin) (point) vanillas)))))
 
 
@@ -1103,10 +1092,17 @@ Only for use by consenting adults."
 (defun proof-execute-minibuffer-cmd ()
   (interactive)
   (let (cmd)
-    (proof-check-process-available 'relaxed)
+    (proof-shell-ready-prover) ;; was (proof-check-process-available 'relaxed) 
     (setq cmd (read-string "Command: " nil 'proof-minibuffer-history))
     (proof-invisible-command cmd 'relaxed)))
 
+
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;
+;; command history  (unfinished)
+;;
 ;; da: below functions for input history simulation are quick hacks.
 ;; Could certainly be made more efficient.
 
@@ -1126,14 +1122,17 @@ Based on position of point."
   ;; proof-next-matching-command)))
       ;; Start a new search
       
-  
-
 (defun proof-next-matching-command (arg)
   "Search through following commands for new command matching current input."
   (interactive "p")
   (proof-previous-matching-command (- arg)))
+
+;;
+;; end command history stuff
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 	  
 
+
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;; Popup and Pulldown Menu ;;;
@@ -1444,11 +1443,6 @@ finish setup which depends on specific proof assistant configuration."
   (setq comment-start-skip 
     (concat (regexp-quote proof-comment-start) "+\\s_?"))
 
-  (setq proof-re-end-of-cmd (concat "\\s_*" proof-terminal-string "\\s_*\\\'"))
-  (setq proof-re-term-or-comment 
-	(concat proof-terminal-string "\\|" (regexp-quote proof-comment-start)
-		"\\|" (regexp-quote proof-comment-end)))
-
   ;; func-menu --- Jump to a goal within a buffer
   (and (boundp 'fume-function-name-regexp-alist)
        (defvar fume-function-name-regexp-proof
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index fb4a5e2e..45220366 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -11,9 +11,89 @@
 
 (require 'proof-config)
 
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;  Starting and stopping the proof-system shell                    ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Internal variables used by shell mode
+;;
+
+(defvar proof-re-end-of-cmd nil 
+  "Regexp matching end of command.  Based on proof-terminal-string.
+Set in proof-shell-mode.")
+
+(defvar proof-re-term-or-comment nil 
+  "Regexp matching terminator, comment start, or comment end.
+Set in proof-shell-mode.")
+
+
+
+
+;;
+;; Implementing the (unfortunately irrelevant) process lock
+;;
+;;
+
+(defvar proof-shell-busy nil 
+  "A lock indicating that the proof shell is processing.
+When this is non-nil, proof-shell-ready-prover will give
+an error.")
+
+;;
+;; History of these horrible functions.
+;;
+;;  proof-check-process-available
+;;    Checks whether the proof process is available.
+;; Specifically:
+;;     (1) Is a proof process running?
+;;     (2) Is the proof process idle?
+;;     (3) Does the current buffer own the proof process?
+;;     (4) Is the current buffer a proof script?
+;; It signals an error if at least one of the conditions is not
+;; fulfilled. If optional arg RELAXED is set, only (1) and (2) are 
+;; tested.
+;;
+;; Later, proof-check-process-available was altered to also
+;; start a proof shell if necessary, although this is also
+;; done (later?) in proof-grab-lock.  It was also altered to
+;; perform configuration for switching scripting buffers.
+;;
+;; Now, we have two functions again:
+;;
+;;  proof-shell-ready-prover   
+;;    starts proof shell, gives error if it's busy.
+;;
+;;  proof-activate-scripting  (in proof-script.el)
+;;    turns on scripting minor mode for current (scripting) buffer.
+;;
+;; Also, a new enabler predicate:
+;;  
+;;  proof-shell-available
+;;    returns non-nil if a proof shell is active and not locked.
+;;
+;; Maybe proof-shell-ready-prover doesn't need to start the shell,
+;; we can find that out later.
+;;
+;; Chasing down 'relaxed' flags:
+;;
+;;   was passed into proof-grab by proof-start-queue
+;;    only call to proof-start-queue with this arg is in
+;;    proof-invisible-command.
+;;   only call of proof-invisible-command with relaxed arg
+;;   is in proof-execute-minibuffer-cmd.
+;;  --- presumably so that command could be executed from any
+;;  buffer, not just a scripting one?
+;;
+;;  I think it's wrong for proof-invisible-command to enforce
+;;  scripting buffer!
+;; 
+;;  This is reflected now by just calling (proof-shell-ready-prover)
+;;  in proof-invisible-command, not proof-check-process-available.
+;;
+;; Hopefully we can get rid of these messy 'relaxed' flags now.
+;;
+;;  -da.
+
+(defun proof-shell-ready-prover ()
+  "Make sure the proof assistant is ready for a command"
+  (proof-start-shell)
+  (if proof-shell-busy (error "Proof Process Busy!")))
 
 (defun proof-shell-live-buffer ()
   "Return buffer of active proof assistant, or nil if none running."
@@ -21,11 +101,39 @@
        (comint-check-proc proof-shell-buffer)
        proof-shell-buffer))
 
+(defun proof-shell-available-p ()
+  "Returns non-nil if there is a proof shell active and available.
+No error messages.  Useful as menu or toolbar enabler."
+  (and (proof-shell-live-buffer)
+       (not proof-shell-busy)))
+
+(defun proof-grab-lock (&optional relaxed)
+  "Grab the proof shell lock."
+  ;; FIXME: this used to observe 'relaxed' flag, now it ignores it!
+  (proof-shell-ready-prover)			;
+  (setq proof-shell-busy t))
+
+(defun proof-release-lock ()
+  "Release the proof shell lock."
+  (if (proof-shell-live-buffer)
+      (progn
+	(if (not proof-shell-busy)
+	    (error "Bug in proof-release-lock: Proof process not busy"))
+	;; da: Removed this now since some commands run from other
+	;; buffers may claim process lock.
+	;; (if (not (member (current-buffer) proof-script-buffer-list))
+	;; (error "Bug in proof-release-lock: Don't own process"))
+	(setq proof-shell-busy nil))))
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;  Starting and stopping the proof-system shell                    ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
 (defun proof-start-shell ()
   "Initialise a shell-like buffer for a proof assistant.
 
 Also generates goal and response buffers.
-Initialises current buffer for scripting.
 Does nothing if proof assistant is already running."
   (if (proof-shell-live-buffer)
       ()
@@ -65,15 +173,7 @@ Does nothing if proof assistant is already running."
 	(set-buffer proof-pbp-buffer)
 	(funcall proof-mode-for-pbp))
 
-      (setq proof-script-buffer-list (list (current-buffer)))
-      (proof-init-segmentation)
-      (setq proof-active-buffer-fake-minor-mode t)
-      (run-hooks 'proof-activate-scripting-hook)
-
-      (if (fboundp 'redraw-modeline)
-	  (redraw-modeline)
-	(force-mode-line-update))
-
+      ;; 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
@@ -405,7 +505,8 @@ error message. At the end it calls `proof-shell-handle-error-hook'. "
 		  (beep)
 
 		  ;; unwind script buffer
-		  (set-buffer (car proof-script-buffer-list))
+		  (if proof-script-buffer-list
+		      (set-buffer (car proof-script-buffer-list)))
 		  (proof-detach-queue)
 		  (delete-spans (proof-locked-end) (point-max) 'type)
 		  (proof-release-lock)
@@ -419,7 +520,8 @@ error message. At the end it calls `proof-shell-handle-error-hook'. "
     (insert-string 
      "Interrupt: Script Management may be in an inconsistent state\n")
     (beep)
-  (set-buffer (car proof-script-buffer-list)))
+  (if proof-script-buffer-list
+      (set-buffer (car proof-script-buffer-list))))
   (if proof-shell-busy
       (progn (proof-detach-queue)
 	     (delete-spans (proof-locked-end) (point-max) 'type)
@@ -538,20 +640,7 @@ assistant."
       (incf i)))
   (save-excursion (proof-shell-insert string)))
 
-(defun proof-grab-lock (&optional relaxed)
-  (proof-start-shell)
-  (proof-check-process-available relaxed)
-  (setq proof-shell-busy t))
 
-(defun proof-release-lock ()
-  (if (proof-shell-live-buffer)
-      (progn
-	(if (not proof-shell-busy)
-	    ; (error "Bug in proof-release-lock: Proof process not busy")
-	    (message "Nag, nag, nag: proof-release-lock: Proof process not busy"))
-	(if (not (member (current-buffer) proof-script-buffer-list))
-	    (error "Bug in proof-release-lock: Don't own process"))
-	(setq proof-shell-busy nil))))
 
 ; Pass start and end as nil if the cmd isn't in the buffer.
 
@@ -591,7 +680,8 @@ Return non-nil if the action list becomes empty; unlock the process
 and removes the queue region.  Otherwise send the next command to the
 proof process."
   (save-excursion
-    (set-buffer (car proof-script-buffer-list))
+    (if proof-script-buffer-list
+	(set-buffer (car proof-script-buffer-list)))
     ;; (if (null proof-action-list) 
     ;;	(error "proof-shell-exec-loop: called with empty proof-action-list."))
     ;; Be more relaxed about calls with empty action list
@@ -687,7 +777,7 @@ arrive."
 	      (string-match (car proof-shell-process-file) message))
 	 (let
 	     ((file (funcall (cdr proof-shell-process-file) message)))
-	   (if (string= file "") 
+	   (if (and proof-script-buffer-list (string= file ""))
 	       (setq file (buffer-file-name (car proof-script-buffer-list))))
 	   (if file
 	       (proof-register-possibly-new-processed-file file))))
@@ -699,7 +789,7 @@ arrive."
 	   (setq proof-included-files-list
 		 (funcall proof-shell-compute-new-files-list message))
 	   (proof-restart-buffers
-	    (remove (car proof-script-buffer-list)
+	    (remove (car-safe proof-script-buffer-list)
 		    (proof-files-to-buffers
 		     (set-difference current-included
 				     proof-included-files-list))))))
@@ -790,9 +880,13 @@ how far we've got."
     
 (defun proof-done-invisible (span) ())
 
+
+;; da: What is the rationale here for making the *command* sent
+;; invisible, rather than the stuff returned????
+;; doc string makes no sense of this.
 (defun proof-invisible-command (cmd &optional relaxed)
   "Send cmd to the proof process without responding to the user."
-  (proof-check-process-available relaxed)
+  (proof-shell-ready-prover)
   (if (not (string-match proof-re-end-of-cmd cmd))
       (setq cmd (concat cmd proof-terminal-string)))
   (proof-start-queue nil nil (list (list nil cmd
@@ -827,7 +921,13 @@ how far we've got."
   (add-hook 'comint-output-filter-functions 'proof-shell-filter nil 'local)
   (setq comint-get-old-input (function (lambda () "")))
   (proof-dont-show-annotations)
-  (setq proof-marker (make-marker)))
+  (setq proof-marker (make-marker))
+
+  (setq proof-re-end-of-cmd (concat "\\s_*" proof-terminal-string "\\s_*\\\'"))
+  (setq proof-re-term-or-comment 
+	(concat proof-terminal-string "\\|" (regexp-quote proof-comment-start)
+		"\\|" (regexp-quote proof-comment-end)))
+  )
 
 (easy-menu-define proof-shell-menu
 		  proof-shell-mode-map
diff --git a/generic/proof-toolbar.el b/generic/proof-toolbar.el
index 2795ea18..f562ed14 100644
--- a/generic/proof-toolbar.el
+++ b/generic/proof-toolbar.el
@@ -200,16 +200,8 @@ Initialised in proof-toolbar-setup.")
 ;; GENERIC PROOF TOOLBAR FUNCTIONS
 ;;
 
-(defun proof-toolbar-process-available-p ()
-  "Enabler for toolbar functions.
-Checks based on those in proof-check-process-available, but
-without giving error messages."
-  (and (eq proof-buffer-type 'script)
-       (proof-shell-live-buffer)
-       (not proof-shell-busy)))
-
 (defun proof-toolbar-undo-enable-p () 
-  (and (proof-toolbar-process-available-p)
+  (and (proof-shell-available-p)
        (> (proof-unprocessed-begin) (point-min))))
 
 (defun proof-toolbar-undo ()
@@ -238,7 +230,7 @@ Move point if the end of the locked position is invisible."
   (proof-goto-end-of-locked-if-pos-not-visible-in-window))
 
 (defun proof-toolbar-retract-enable-p ()
-  (and (proof-toolbar-process-available-p)
+  (and (proof-shell-available-p)
        (member (current-buffer) proof-script-buffer-list)))
 
 (defun proof-toolbar-retract ()
@@ -282,7 +274,7 @@ Move point if the end of the locked position is invisible."
 
 (defun proof-toolbar-qed-enable-p ()
   (and proof-shell-proof-completed
-       (proof-toolbar-process-available-p)))
+       (proof-shell-available-p)))
 
 (defun proof-toolbar-qed () 
   "Insert a save theorem command into the script buffer, issue it."