diff options
Diffstat (limited to 'generic/proof-script.el')
| -rw-r--r-- | generic/proof-script.el | 14 |
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." |