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-script.el | 16 +++++++---------
 1 file changed, 7 insertions(+), 9 deletions(-)

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

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