diff options
| author | David Aspinall | 1999-11-29 12:46:23 +0000 |
|---|---|---|
| committer | David Aspinall | 1999-11-29 12:46:23 +0000 |
| commit | debfa48c5cda791a4e8939918936f3ed5713d4d2 (patch) | |
| tree | d3031cfaeea0d630c5c34349a3aec30ff4154a52 /generic | |
| parent | a166643ad31a9a1be7c546709c8c2d59d056873a (diff) | |
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.
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/proof-shell.el | 20 |
1 files changed, 17 insertions, 3 deletions
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. |