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

1 files changed, 7 insertions, 7 deletions

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."