From debfa48c5cda791a4e8939918936f3ed5713d4d2 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Mon, 29 Nov 1999 12:46:23 +0000 Subject: Comments about improved handling of urgent message markers, following jrl's bug report about duplication of occasional urgent messages. The correct fix is to set proof-shell-eager-annotation-start-length properly. --- generic/proof-shell.el | 20 +++++++++++++++++--- 1 file changed, 17 insertions(+), 3 deletions(-) (limited to 'generic') diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 4fbdceee..b0c09c52 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -1096,6 +1096,11 @@ proof-shell-exec-loop, to process the next item." ;; before using proof-shell-insert. (set-marker proof-marker (point)) + ;; FIXME: possible improvement. Make for post 3.0 releases + ;; in case of problems. + ;; (set-marker proof-shell-urgent-message-marker (point)) + ;; (set-marker proof-shell-urgent-message-scanner (point)) + ;; FIXME da: this space fudge is actually a visible hack: ;; the response string begins with a space and a newline. (insert proof-shell-insert-space-fudge) @@ -1443,12 +1448,21 @@ This is a subroutine of proof-shell-filter." ;; If the search for the starting annotation was unsuccessful, ;; set the scanner marker to the limit of the last search for ;; the starting annotation, less the maximal length of the - ;; annotation. + ;; annotation. (set-marker proof-shell-urgent-message-scanner (min - (- (point) proof-shell-eager-annotation-start-length) - (1- (process-mark (get-buffer-process (current-buffer)))))) + ;; NB: possible fix here not included: a test to be sure we + ;; don't go back before the start of the command! This + ;; fixes a minor problem which is possible duplication + ;; of urgent messages which are less than + ;; proof-shell-eager-annotation-start-length characters. + ;; But if proof-general is configured properly, there + ;; should never be any such messages! + ;; (max + ;; (marker-position proof-marker) + (- (point) proof-shell-eager-annotation-start-length) + (1- (process-mark (get-buffer-process (current-buffer))))))) ;; Otherwise, the search for the ending annotation was ;; unsuccessful, so we set the scanner marker to the start of ;; the annotation found. -- cgit v1.2.3