From 428235d44085f32f47557d921fbb2057a2996df2 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Tue, 26 May 2009 13:21:18 +0000
Subject: proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window: obey
 proof-follow-mode=ignore.  Ref
 http://proofgeneral.inf.ed.ac.uk/trac/ticket/187

---
 generic/proof-script.el | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

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

diff --git a/generic/proof-script.el b/generic/proof-script.el
index d9ef6d44..b3d1fb3d 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -479,14 +479,14 @@ Does nothing if there is no active scripting buffer, or if
 Intended as a hook function for `proof-shell-handle-error-or-interrupt-hook'."
   (interactive)
   (cond
+   ((eq proof-follow-mode 'ignore))
    ((eq proof-shell-error-or-interrupt-seen 'error)
-    (proof-goto-end-of-locked-if-pos-not-visible-in-window))
-   ((eq proof-shell-error-or-interrupt-seen 'interrupt)
-    (proof-with-current-buffer-if-exists
-     proof-script-buffer
-     ;; Give a hint of how to jump to the end of locked, unless visible.
-     (unless (proof-end-of-locked-visible-p)
-       (pg-jump-to-end-hint))))))
+    (proof-goto-end-of-locked-if-pos-not-visible-in-window)))
+  (proof-with-current-buffer-if-exists
+   proof-script-buffer
+   ;; Give a hint of how to jump to the end of locked, unless visible.
+   (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