aboutsummaryrefslogtreecommitdiff
path: root/plastic
diff options
context:
space:
mode:
Diffstat (limited to 'plastic')
-rw-r--r--plastic/plastic.el7
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))