Many robustness improvements for error and interrupt handling:

- Introduce proof-shell-error-or-interrupt-seen flag set after an error
or interrupt was seen (in fact, on every call to proof-release-lock).
Examine it in proof-activate-scripting to see whether hooks succeeded
in activating scripting.
- Test in the shell filter for the lock being held yet nothing in the
action list, and clear the lock if so.  Gets rid of repetetive
proof-shell-busy messages when the queue is empty (for errors during
development, or nasty uses of C-g)
- Add a timeout to proof-shell-wait  (not used yet)

7 files changed, 172 insertions, 94 deletions

diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 074871be..96afb403 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -1157,11 +1157,11 @@ All locked regions are cleared and the active scripting buffer
 deactivated.  
 
 If the proof shell is busy, an interrupt is sent with
-@code{proof-interrupt-process} and we wait until the process is ready. 
+@code{proof-interrupt-process} and we wait until the process is ready.
 
 The restart command should re-synchronize Proof General with the proof
 assistant, without actually exiting and restarting the proof assistant
-process.  
+process.
 
 It is up to the proof assistant how much context is cleared: for
 example, theories already loaded may be "cached" in some way,
@@ -1275,11 +1275,11 @@ All locked regions are cleared and the active scripting buffer
 deactivated.  
 
 If the proof shell is busy, an interrupt is sent with
-@code{proof-interrupt-process} and we wait until the process is ready. 
+@code{proof-interrupt-process} and we wait until the process is ready.
 
 The restart command should re-synchronize Proof General with the proof
 assistant, without actually exiting and restarting the proof assistant
-process.  
+process.
 
 It is up to the proof assistant how much context is cleared: for
 example, theories already loaded may be "cached" in some way,
@@ -3302,9 +3302,11 @@ shell variables:
 This is the bare minimum needed to get a shell buffer and
 its friends configured in the function @code{proof-shell-start}.
 @end defvar
-@c TEXI DOCSTRING MAGIC: proof-shell-handle-error-hook
-@defvar proof-shell-handle-error-hook 
-Hooks run after an error has been reported in the response buffer.
+@c TEXI DOCSTRING MAGIC: proof-shell-handle-error-or-interrupt-hook
+@defvar proof-shell-handle-error-or-interrupt-hook 
+Run after an error or interrupt has been reported in the response buffer.@*
+Hook functions may inspect @samp{@code{proof-shell-error-or-interrupt-seen}} to 
+determine whether the cause was an error or interrupt.
 @end defvar
 
 @c TEXI DOCSTRING MAGIC: proof-shell-process-output-system-specific
@@ -3926,6 +3928,14 @@ If non-nil, the value counts the commands from the last command
 of the proof (starting from 1).
 @end defvar
 
+@c TEXI DOCSTRING MAGIC: proof-shell-error-or-interrupt-seen
+
+
+@defvar proof-shell-error-or-interrupt-seen 
+Flag indicating that an error or interrupt has just occurred.@*
+Set to @code{'error} or @code{'interrupt} if one was observed from the proof 
+assistant during the last group of commands.
+@end defvar
 The @file{proof.el} also loads @file{proof-config.el} which declares the
 proof assistant configuration variables for Proof General.
 For details, @xref{Adapting Proof General to Other Provers}.
@@ -4287,11 +4297,11 @@ All locked regions are cleared and the active scripting buffer
 deactivated.  
 
 If the proof shell is busy, an interrupt is sent with
-@code{proof-interrupt-process} and we wait until the process is ready. 
+@code{proof-interrupt-process} and we wait until the process is ready.
 
 The restart command should re-synchronize Proof General with the proof
 assistant, without actually exiting and restarting the proof assistant
-process.  
+process.
 
 It is up to the proof assistant how much context is cleared: for
 example, theories already loaded may be "cached" in some way,
diff --git a/generic/proof-config.el b/generic/proof-config.el
index cf03c487..4f0e05f1 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -1353,9 +1353,11 @@ its friends configured in the function proof-shell-start."
   :type '(repeat function)
   :group 'proof-shell)
 
-(defcustom proof-shell-handle-error-hook
+(defcustom proof-shell-handle-error-or-interrupt-hook
   '(proof-goto-end-of-locked-if-pos-not-visible-in-window)
-  "Hooks run after an error has been reported in the response buffer."
+  "Run after an error or interrupt has been reported in the response buffer.
+Hook functions may inspect `proof-shell-error-or-interrupt-seen' to 
+determine whether the cause was an error or interrupt."
   :type '(repeat function)
   :group 'proof-shell)
 
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 22f78511..6a98a8a2 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -44,9 +44,6 @@
 	    proof-shell-invisible-command)))
 ;; proof-response-buffer-display now in proof.el, removed from above.
 
-;; FIXME: *variable* proof-shell-proof-completed is declared in proof-shell
-;; and used here.  Should be moved to proof.el or removed from here.
-
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
 ;;  Internal variables used by script mode
@@ -342,7 +339,7 @@ Must be an active scripting buffer."
 
 (defun proof-goto-end-of-locked-if-pos-not-visible-in-window ()
   "If the end of the locked region is not visible, jump to the end of it.
-A possible hook function for proof-shell-handle-error-hook.
+A possible hook function for proof-shell-handle-error-or-interrupt-hook.
 Does nothing if there is no active scripting buffer."
   (interactive)
   (if proof-script-buffer
@@ -813,9 +810,28 @@ correct theory, or whatever."
       ;; to block.   NB: The hook function may send commands to the
       ;; process which will re-enter this function, but should exit 
       ;; immediately because scripting has been turned on now.
-      (let
-	  ((activated-interactively	(interactive-p)))
-	(run-hooks 'proof-activate-scripting-hook))))))
+      (if proof-activate-scripting-hook
+	  (let
+	      ((activated-interactively	(interactive-p)))
+	    ;; Clear flag in case no hooks run shell commands
+	    (setq proof-shell-error-or-interrupt-seen nil)
+	    (run-hooks 'proof-activate-scripting-hook)
+	    ;; In case the activate scripting functions
+	    ;; caused an error in the proof assistant, we'll
+	    ;; consider activating scripting to have failed,
+	    ;; and raise an error here.
+	    ;; (Since this behaviour is intimate with the hook functions,
+	    ;;  it could be removed and left to implementors of 
+	    ;;  specific instances of PG).
+	    ;; FIXME: we could consider simply running the hooks
+	    ;; as the last step before turning on scripting properly,
+	    ;; provided the hooks don't inspect proof-script-buffer.
+	    (if proof-shell-error-or-interrupt-seen
+		(progn
+		  (proof-deactivate-scripting) ;; turn it off again!
+		  ;; Give an error to prevent further actions.
+		  (error "Proof General: Scripting not activated because of error or interrupt.")))))))))
+
 
 (defun proof-toggle-active-scripting (&optional arg)
   "Toggle active scripting mode in the current buffer.
@@ -904,7 +920,7 @@ With ARG, turn on scripting iff ARG is positive."
 
 ;; da: NEW function added 28.10.98.
 ;; This is used by toolbar follow mode (which used to use the function
-;; above).  [But wouldn't work for proof-shell-handle-error-hook?].
+;; above).  [But wouldn't work for proof-shell-handle-error-or-interrupt-hook?].
 
 (defun proof-goto-end-of-queue-or-locked-if-not-visible ()
   "Jump to the end of the queue region or locked region if it isn't visible.
@@ -1742,6 +1758,15 @@ value of proof-locked span."
   "Remove all spans from scripting buffers via proof-restart-buffers."
   (proof-restart-buffers (proof-script-buffers-with-spans)))
 
+(defun proof-script-clear-queue-spans ()
+  "If there is an active scripting buffer, remove the queue span from it.
+This is a subroutine used in proof-shell-handle-{error,interrupt}."
+  (if proof-script-buffer
+      (with-current-buffer proof-script-buffer
+	(proof-detach-queue)
+	;; FIXME da: point-max seems a bit excessive here,
+	;; proof-queue-or-locked-end should be enough.
+	(delete-spans (proof-locked-end) (point-max) 'type))))
 
 ;; A command for making things go horribly wrong - it moves the
 ;; end-of-locked-region marker backwards, so user had better move it
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 6fb67920..51b6f2e9 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -37,6 +37,7 @@
 	    proof-detach-queue 
 	    proof-locked-end 
 	    proof-set-queue-endpoints
+	    proof-script-clear-queue-spans
 	    proof-file-to-buffer 
 	    proof-register-possibly-new-processed-file
 	    proof-restart-buffers)))
@@ -167,24 +168,18 @@ No error messages.  Useful as menu or toolbar enabler."
 (defun proof-grab-lock (&optional queuemode)
   "Grab the proof shell lock, starting the proof assistant if need be.
 Runs proof-state-change-hook to notify state change.
+Clears the proof-shell-error-or-interrupt-seen flag.
 If QUEUEMODE is supplied, set the lock to that value."
   (proof-shell-ready-prover)
+  (setq proof-shell-error-or-interrupt-seen nil)
   (setq proof-shell-busy (or queuemode t))
   (run-hooks 'proof-state-change-hook))
 
-(defun proof-release-lock ()
-  "Release the proof shell lock."
-  ; da: this test seems somewhat worthless
-  ; (if (proof-shell-live-buffer)
-  ; (progn
-	; da: Removed this so that persistent users are allowed to
-	; type in the process buffer without being hassled.
-	;(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 (eq (current-buffer) proof-script-buffer))
-	; (error "Bug in proof-release-lock: Don't own process"))
+(defun proof-release-lock (&optional err-or-int)
+  "Release the proof shell lock, with error or interrupt flag ERR-OR-INT.
+Clear proof-shell-busy, and set proof-shell-error-or-interrupt-seen
+to err-or-int."
+  (setq proof-shell-error-or-interrupt-seen err-or-int)
   (setq proof-shell-busy nil))
 
 
@@ -306,6 +301,11 @@ Does nothing if proof assistant is already running."
 	;; present.
 	(and (fboundp 'toggle-enable-multibyte-characters)
 	     (toggle-enable-multibyte-characters -1))
+	
+	;; Initialise shell mode 
+	;; Q: should this be done every time the process is started?
+	;; A: yes, it does the process initialization, which is a bit
+	;; odd (would expect it to be done here, maybe).
 
 
 	(funcall proof-mode-for-shell)
@@ -410,10 +410,12 @@ exited by hand (or exits by itself)."
       (if proc (set-process-sentinel proc nil))
       ;; Restart all scripting buffers
       (proof-script-remove-all-spans-and-deactivate)
-      ;; Clear state
+      ;; Clear state (some of these not strictly necessary)
       (setq proof-included-files-list nil
 	    proof-shell-busy nil
-	    proof-shell-proof-completed nil)
+	    proof-shell-proof-completed nil
+	    proof-shell-error-or-interrupt-seen nil
+	    proof-shell-action-list nil)
       ;; Kill buffers associated with shell buffer
       (if (buffer-live-p proof-goals-buffer)
 	  (progn 
@@ -452,11 +454,11 @@ All locked regions are cleared and the active scripting buffer
 deactivated.  
 
 If the proof shell is busy, an interrupt is sent with
-proof-interrupt-process and we wait until the process is ready. 
+proof-interrupt-process and we wait until the process is ready.
 
 The restart command should re-synchronize Proof General with the proof
 assistant, without actually exiting and restarting the proof assistant
-process.  
+process.
 
 It is up to the proof assistant how much context is cleared: for
 example, theories already loaded may be \"cached\" in some way,
@@ -472,8 +474,9 @@ object files, used by Lego and Coq)."
   (proof-script-remove-all-spans-and-deactivate)
   (setq proof-included-files-list nil
 	proof-shell-busy nil
-	proof-shell-proof-completed nil
-	proof-action-list nil)
+	proof-action-list nil
+	proof-shell-error-or-interrupt-seen nil
+	proof-shell-proof-completed nil)
   (if (and (buffer-live-p proof-shell-buffer)
 	   proof-shell-restart-cmd)
 	   (proof-shell-invisible-command
@@ -906,18 +909,20 @@ See the documentation for `proof-shell-delayed-output' for further details."
 ;;
 ;; 
 
+
+
 ;; FIXME da: the magical use of "Done." and "done" as values in
 ;; proof-shell-handled-delayed-output is horrendous.  Should
 ;; be changed to something more understandable!!
 
 (defun proof-shell-handle-error (cmd string)
   "React on an error message triggered by the prover.
-Called with shell buffer current.
 We first flush unprocessed goals to the goals buffer.
-The error message is displayed in the `proof-response-buffer'.
-Then we call `proof-shell-handle-error-hook'. "
+The error message is displayed in the responsebuffer.
+Then we call `proof-shell-error-or-interrupt-action', which see."
 
-  ;; flush goals
+  ;; FIXME: this is messy, should be done in a subroutine.
+  ;; Why not also for interrupts anyway?
   (unless
       (equal proof-shell-delayed-output (cons 'insert "Done."))
     (save-excursion
@@ -934,11 +939,6 @@ Then we call `proof-shell-handle-error-hook'. "
 ;        (proof-fontify-region (point-min) (point-max))
 ;	(proof-display-and-keep-buffer proof-goals-buffer)))
 
-  ;; This prevents problems if the user types in the
-  ;; shell buffer: without it the same error is seen by
-  ;; the proof-shell filter over and over.
-  (setq proof-action-list nil)
-
   ;; Perhaps we should erase the buffer in proof-response-buffer, too?
 
     ;; We extract all text between text matching
@@ -953,32 +953,37 @@ Then we call `proof-shell-handle-error-hook'. "
    proof-shell-error-regexp proof-shell-annotated-prompt-regexp
    'proof-error-face)
 
-  
-  (save-excursion ;current-buffer
-    (proof-display-and-keep-buffer proof-response-buffer)
-		  (beep)
-
-		  ;; unwind script buffer
-		  (if proof-script-buffer
-		      (with-current-buffer proof-script-buffer
-			(proof-detach-queue)
-			(delete-spans (proof-locked-end) (point-max) 'type)))
-		  (proof-release-lock)
-		  (run-hooks 'proof-shell-handle-error-hook)))
-
-;; FIXME da: this function is a mess.
+  (proof-display-and-keep-buffer proof-response-buffer)
+  (proof-shell-error-or-interrupt-action 'error))
+
 (defun proof-shell-handle-interrupt ()
+   "React on an interrupt message from the prover.
+ Runs proof-shell-error-or-interrupt-action."
   (proof-shell-maybe-erase-response t t t)
+  (proof-shell-handle-output
+   proof-shell-interrupt-regexp proof-shell-annotated-prompt-regexp
+   'proof-error-face)
+;  (proof-display-and-keep-buffer proof-response-buffer)
   (proof-warning 
    "Interrupt: script management may be in an inconsistent state")
-  (beep)
-  (if (and proof-shell-busy proof-script-buffer)
-      (with-current-buffer proof-script-buffer
-	(proof-detach-queue)
-	;; FIXME: point-max seems a bit excessive here
-	(delete-spans (proof-locked-end) (point-max) 'type)))
-  (setq proof-action-list nil)
-  (proof-release-lock))
+  (proof-shell-error-or-interrupt-action 'interrupt))
+
+(defun proof-shell-error-or-interrupt-action (&optional err-or-int)
+  "General action when an error or interrupt message appears from prover.
+A subroutine for proof-shell-handle-interrupt and proof-shell-handle-error.
+
+We sound a beep, clear queue spans and proof-action-list, and set the flag 
+proof-shell-error-or-interrupt-seen to the ERR-OR-INT argument.
+Then we call `proof-shell-handle-error-or-interrupt-hook'."
+  (save-excursion			;; for safety.
+    (beep)
+    ;; NB: previously for interrupt, clear-queue-spans 
+    ;; was only called if shell busy.  Any harm calling it always?
+    (proof-script-clear-queue-spans) 
+    (setq proof-action-list nil)
+    (proof-release-lock err-or-int)
+    ;; New: this is called for interrupts too.
+    (run-hooks 'proof-shell-handle-error-or-interrupt-hook)))
 
 (defun proof-goals-pos (span maparg)
   "Given a span, return the start of it if corresponds to a goal, nil otherwise."
@@ -1211,14 +1216,7 @@ The queue mode is set to 'advancing"
   (proof-append-alist alist 'advancing))
 
 
-; returns t if it's run out of input
-
 
-;; 
-;; The loop looks like: Execute the
-; command, and if it's successful, do action on span.  If the
-; command's not successful, we bounce the rest of the queue and do
-; some error processing.
 
 (defun proof-shell-exec-loop () 
   "Process the proof-action-list.
@@ -1234,7 +1232,12 @@ the action list becomes empty, unlock the process and remove the queue
 region.
 
 The return value is non-nil if the action list is now empty."
-  (or (not proof-action-list)		; exit immediately if finished.
+  ;; The loop looks like: Execute the
+  ;; command, and if it's successful, do action on span.  If the
+  ;; command's not successful, we bounce the rest of the queue and do
+  ;; some error processing.
+
+  (unless (not proof-action-list)		; exit immediately if finished.
       (save-excursion
 	;; Switch to active scripting buffer if there is one.
 	(if proof-script-buffer
@@ -1597,8 +1600,16 @@ however, are always processed; hence their name)."
 		      ;; (proof-fontify-region startpos (point))
 		      (setq string (buffer-substring startpos (point)))
 		      (goto-char (point-max))	
-		      (proof-shell-filter-process-output string)))))))))
-
+		      (proof-shell-filter-process-output string))))
+	    ;; If proof-action-list is empty, make sure the process lock
+	    ;; is not held!  This should solve continual "proof shell busy"
+	    ;; error messages which sometimes occur during development,
+	    ;; at least.
+	    (if proof-shell-busy
+		(progn
+		  (proof-debug 
+		   "proof-shell-filter found empty action list yet proof shell busy.")
+		  (proof-clear-lock))))))))
 
 
 (defun proof-shell-filter-process-output (string)
@@ -1670,13 +1681,13 @@ XEmacs only."
 ;; proof-shell-invisible-command: used to implement user-level commands.
 ;;
 
-(defun proof-shell-wait ()
-  "Busy wait for proof-shell-busy to become nil.
+(defun proof-shell-wait (&optional timeout)
+  "Busy wait for proof-shell-busy to become nil, or for TIMEOUT seconds.
 Needed between sequences of commands to maintain synchronization,
-because Proof General does not allow for the action list to be extended.
-May be called by proof-shell-invisible-command."
+because Proof General does not allow for the action list to be extended
+in some cases.   May be called by proof-shell-invisible-command."
   (while proof-shell-busy
-    (accept-process-output nil)
+    (accept-process-output nil timeout)
     (sit-for 0)))
 
 
@@ -1719,9 +1730,15 @@ before and after sending the command."
 (define-derived-mode proof-shell-mode comint-mode 
   "proof-shell" "Proof General shell mode class for proof assistant processes"
   (setq proof-buffer-type 'shell)
-  (setq proof-shell-busy nil)
-  (setq proof-shell-delayed-output (cons 'insert "done"))
-  (setq proof-shell-proof-completed nil)
+  
+  ;; Clear state
+  (setq proof-shell-busy nil
+	proof-shell-delayed-output (cons 'insert "done")
+	proof-shell-proof-completed nil
+	;; FIXME: these next two probably not necessary
+	proof-shell-error-or-interrupt-seen nil
+	proof-shell-action-list nil)
+
   (make-local-variable 'proof-shell-insert-hook)
 
   ;; comint customisation. comint-prompt-regexp is used by
diff --git a/generic/proof.el b/generic/proof.el
index 741e4a01..adeac019 100644
--- a/generic/proof.el
+++ b/generic/proof.el
@@ -132,6 +132,11 @@ read.")
 (defvar proof-response-buffer nil
   "The response buffer.")
 
+(defvar proof-shell-error-or-interrupt-seen nil
+  "Flag indicating that an error or interrupt has just occurred.
+Set to 'error or 'interrupt if one was observed from the proof 
+assistant during the last group of commands.")
+
 (defvar proof-shell-proof-completed nil
   "Flag indicating that a completed proof has just been observed.
 If non-nil, the value counts the commands from the last command
@@ -408,7 +413,9 @@ The warning is coloured with proof-warning-face."
 If proof-show-debug-messages is nil, do nothing."
   (if proof-show-debug-messages
       (progn
-	(proof-response-buffer-display (apply 'concat args) 
+	(proof-response-buffer-display (apply 'concat 
+					      "PG debug: " 
+					      args)
 				       'proof-debug-message-face)
 	(proof-display-and-keep-buffer proof-response-buffer))))
 
diff --git a/isa/isa.el b/isa/isa.el
index c4d72822..1592feab 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -257,7 +257,22 @@ and script mode."
    (format "ProofGeneral.%supdate_thy_only \"%s\";"
 	   (if try "try_" "") (file-name-sans-extension file))
    wait))
-  
+
+;; Experiments for background non-blocking loading of theory: this is
+;; quite difficult, actually: we need to set a callback from 
+;; proof-done-invisible to take the final step in switching on
+;; scripting.  We may be able to pass the hook argument into the
+;; action list using the "span" argument which means nothing for
+;; invisible command usually.
+
+;(defun isa-update-error (&rest args)
+;  "Callback for proof-invisible-command.
+;In case an update leads to an error/interrupt in Isabelle, 
+;we make sure scripting is deactivated and raise an elisp error."
+;  (if proof-shell-error-or-interrupt-seen
+;      (proof-deactivate-scripting))
+;  (proof-shell-done-invisible "Isabelle Proof General: error during use_thy, scripting not activated!"))
+
 (defun isa-shell-update-thy ()
   "Possibly issue update_thy_only command to Isabelle.
 If the current buffer has an empty locked region, the interface is
@@ -278,8 +293,9 @@ This is a hook function for proof-activate-scripting-hook."
 	(isa-update-thy-only buffer-file-name t 
 			     ;; whether to block or not
 			     (if (and (boundp 'activated-interactively)
-				      activated-interactively)
-				 nil t))
+					activated-interactively)
+				 t ; was nil, but will falsely leave Scripting on! 
+			       t))
 	;; Leave the messages from the update around.
 	(setq proof-shell-erase-response-flag nil))))
 
diff --git a/plastic/plastic.el b/plastic/plastic.el
index dd9aa6e5..a8a1e6b1 100644
--- a/plastic/plastic.el
+++ b/plastic/plastic.el
@@ -476,10 +476,10 @@ Given is the first SPAN which needs to be undone."
 
   (add-hook 'proof-pre-shell-start-hook    'plastic-pre-shell-start nil t)
   (add-hook 'proof-shell-insert-hook       'plastic-shell-adjust-line-width)
-  (add-hook 'proof-shell-handle-error-hook 'plastic-had-error)
+  (add-hook 'proof-shell-handle-error-or-interrupt-hook 'plastic-had-error)
   (add-hook 'proof-shell-insert-hook       'plastic-preprocessing)
 
-;; (add-hook 'proof-shell-handle-error-hook 
+;; (add-hook 'proof-shell-handle-error-or-interrupt-hook 
 ;; (lambda()(goto-char (search-forward (char-to-string  proof-terminal-char)))))
 
 ;;  (add-hook 'proof-shell-handle-delayed-output-hook `plastic-show-shell-buffer t)
@@ -678,7 +678,8 @@ We assume that module identifiers coincide with file names."
 
 (defun plastic-had-error ()
     "sets var plastic-error-occurred, called from hook"
-    (setq plastic-error-occurred t))
+    (if (eq proof-shell-error-or-interrupt-seen 'error)
+	(setq plastic-error-occurred t)))
 (defun plastic-reset-error ()
     "UNsets var plastic-error-occurred, before minibuffer or try cmd"
     (setq plastic-error-occurred nil))