diff options
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/pg-goals.el | 47 |
1 files changed, 24 insertions, 23 deletions
diff --git a/generic/pg-goals.el b/generic/pg-goals.el index 8edbc42a..5b2e88de 100644 --- a/generic/pg-goals.el +++ b/generic/pg-goals.el @@ -86,47 +86,48 @@ May enable proof-by-pointing or similar features. Converts term substructure markup into mouse-highlighted extents, and properly fontifies STRING using proof-fontify-region." (save-excursion - ;; Response buffer may be out of date. It may contain (error) - ;; messages relating to earlier proof states - - ;; FIXME da: this isn't always the case. In Isabelle - ;; we get <WARNING MESSAGE> <CURRENT GOALS> output, - ;; or <WARNING MESSAGE> <ORDINARY MESSAGE>. Both times - ;; <WARNING MESSAGE> would be relevant. - ;; We should only clear the output that was displayed from - ;; the *previous* prompt. - - ;; Erase the response buffer if need be, maybe also removing the - ;; window. Indicate that it should be erased before the next - ;; output. - (proof-shell-maybe-erase-response t t) - - ;; Erase the goals buffer and add in the new string - (set-buffer proof-goals-buffer) - (erase-buffer) + ;; Response buffer may be out of date. It may contain (error) + ;; messages relating to earlier proof states + + ;; FIXME da: this isn't always the case. In Isabelle + ;; we get <WARNING MESSAGE> <CURRENT GOALS> output, + ;; or <WARNING MESSAGE> <ORDINARY MESSAGE>. Both times + ;; <WARNING MESSAGE> would be relevant. + ;; We should only clear the output that was displayed from + ;; the *previous* prompt. + + ;; Erase the response buffer if need be, maybe removing the + ;; window. Indicate it should be erased before the next output. + (proof-shell-maybe-erase-response t t) + + ;; Erase the goals buffer and add in the new string + (set-buffer proof-goals-buffer) + (erase-buffer) + ;; Only bother processing and displaying, etc, if string is + ;; non-empty. + (unless (string-equals string "") (insert string) (if pg-use-specials-for-fontify ;; With special chars for fontification, do that first, ;; but keep specials in case also used for subterm markup. (proof-fontify-region (point-min) (point-max) 'keepspecials)) - (pg-goals-analyse-structure (point-min) (point-max)) (unless pg-use-specials-for-fontify ;; provers which use ordinary keywords to fontify output must ;; do fontification second after subterm specials are removed. (proof-fontify-region (point-min) (point-max))) - + ;; Record a cleaned up version of output string (setq proof-shell-last-output (buffer-substring (point-min) (point-max))) - + (set-buffer-modified-p nil) ; nicety - + ;; Keep point at the start of the buffer. (proof-display-and-keep-buffer - proof-goals-buffer (point-min)))) + proof-goals-buffer (point-min))))) (defun pg-goals-analyse-structure (start end) |