From 1604db92ae0d21b58caafb481aef73570056a122 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Fri, 1 Oct 2010 15:07:07 +0000
Subject: proof-shell-handle-error-or-interrupt-hook: only run if ordinary
 scripting input (no non-nil flags in queue)

---
 generic/proof-shell.el | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

(limited to 'generic/proof-shell.el')

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."
-- 
cgit v1.2.3