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, 4 insertions, 3 deletions

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