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)

1 files changed, 8 insertions, 1 deletions

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))))