diff options
Diffstat (limited to 'generic/proof-script.el')
| -rw-r--r-- | generic/proof-script.el | 16 |
1 files changed, 4 insertions, 12 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index 0f32ccdd..ec6684af 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -535,16 +535,6 @@ Intended as a hook function for `proof-shell-handle-error-or-interrupt-hook'." (win (and pos (get-buffer-window proof-script-buffer t)))) (and win (pos-visible-in-window-p pos)))) -;; Simplified version of above for toolbar follow mode -- which wouldn't -;; work with abouve because of proof-shell-handle-error-or-interrupt-hook[?] -(defun proof-goto-end-of-queue-or-locked-if-not-visible () - "Jump to the end of the queue region or locked region if it isn't visible. -Assumes script buffer is current" - (unless (pos-visible-in-window-p - (proof-queue-or-locked-end) - (get-buffer-window (current-buffer) t)) - (goto-char (proof-queue-or-locked-end)))) - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -2372,6 +2362,7 @@ Span deletion property set to flag DELETE-REGION." (defun proof-last-goal-or-goalsave () + "Return the span which is the last goal or save before point." (save-excursion (let ((span (span-at-before (proof-locked-end) 'type))) (while (and span @@ -3060,9 +3051,10 @@ Choice of function depends on configuration setting." start)) (if (and (markerp proof-overlay-arrow) (marker-position proof-overlay-arrow) - (< start (marker-position proof-overlay-arrow)) + ; only move marker up: + ;(< start (marker-position proof-overlay-arrow)) (>= start (proof-queue-or-locked-end))) - (proof-set-overlay-arrow start))) + (proof-set-overlay-arrow (proof-queue-or-locked-end)))) (defun proof-script-set-after-change-functions () "Set `after-change-functions' for script buffers." |