proof-shell-handle-error-or-interrupt-hook: only run if ordinary scripting input (no non-nil flags in queue)

2 files changed, 15 insertions, 12 deletions

diff --git a/generic/proof-script.el b/generic/proof-script.el
index 88bfb720..63d185ed 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -446,7 +446,6 @@ Does nothing if there is no active scripting buffer, or if
 `proof-follow-mode' is set to 'ignore."
   (interactive)
   (if (and proof-script-buffer
-	   (not proof-autosend-running)
 	   (not (eq proof-follow-mode 'ignore)))
       (unless (proof-end-of-locked-visible-p)
 	(proof-goto-end-of-locked t))))
@@ -455,14 +454,13 @@ Does nothing if there is no active scripting buffer, or if
   "As `proof-goto-end-of-locked-if-pos-not-visible-in-window', but not for interrupts.
 Intended as a hook function for `proof-shell-handle-error-or-interrupt-hook'."
   (interactive)
-  (unless proof-autosend-running
-    (unless (eq proof-follow-mode 'ignore)
-      (if (eq proof-shell-last-output-kind 'error)
-	  (proof-goto-end-of-locked-if-pos-not-visible-in-window)))
-    (proof-with-current-buffer-if-exists
-      proof-script-buffer
-      (unless (proof-end-of-locked-visible-p)
-	(pg-jump-to-end-hint)))))
+  (unless (eq proof-follow-mode 'ignore)
+    (if (eq proof-shell-last-output-kind 'error)
+	(proof-goto-end-of-locked-if-pos-not-visible-in-window)))
+  (proof-with-current-buffer-if-exists
+   proof-script-buffer
+   (unless (proof-end-of-locked-visible-p)
+     (pg-jump-to-end-hint))))
 
 (defun proof-end-of-locked-visible-p ()
   "Return non-nil if end of locked region is visible."
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 445107b7..aaff5673 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -597,7 +597,11 @@ didn't cause prover output."
   "Take action on errors or interrupts.
 ERR-OR-INT is a flag, 'error or 'interrupt.
 This is a subroutine of `proof-shell-handle-error-or-interrupt'.
-Must be called with proof shell buffer current."
+Must be called with proof shell buffer current.
+
+This function invokes `proof-shell-handle-error-or-interrupt-hook'
+unless the FLAGS for the command are non-nil (indicating errors
+are ignored somehow)."
   (unless proof-shell-quiet-errors
     (beep))
   (let* ((fatalitem  (car-safe proof-action-list))
@@ -613,8 +617,9 @@ Must be called with proof shell buffer current."
     (unless flags
       ;; Give a hint about C-c C-`.  (NB: approximate test)
       (if (pg-response-has-error-location)
-	  (pg-next-error-hint)))
-    (run-hooks 'proof-shell-handle-error-or-interrupt-hook)))
+	  (pg-next-error-hint))
+      ;; Run hooks for additional effects, e.g. highlight or moving pointer
+      (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."