From 78ae7490e865acb74f1b4ca2c5805e95045b5c22 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Wed, 11 Sep 2002 21:39:35 +0000 Subject: Short-circuit goals display if string empty. --- generic/pg-goals.el | 47 ++++++++++++++++++++++++----------------------- 1 file 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 output, - ;; or . Both times - ;; 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 output, + ;; or . Both times + ;; 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) -- cgit v1.2.3