diff options
author | David Aspinall <da@inf.ed.ac.uk> | 2005-07-27 12:38:33 +0000 |
---|---|---|
committer | David Aspinall <da@inf.ed.ac.uk> | 2005-07-27 12:38:33 +0000 |
commit | 0b676d8a5726f22088aa754362af61228a733d0b (patch) | |
tree | 7d465710c5f574a7bacee64eed06f92834e04be6 | |
parent | fc1c3f61737da67ff63532d5c201d16e455e8af2 (diff) |
Resolve buffer for background resolution prover (Claire Quigley)
-rw-r--r-- | generic/pg-resolve.el | 220 |
1 files changed, 220 insertions, 0 deletions
diff --git a/generic/pg-resolve.el b/generic/pg-resolve.el new file mode 100644 index 00000000..8a683a0b --- /dev/null +++ b/generic/pg-resolve.el @@ -0,0 +1,220 @@ + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; +;; Displaying in the response buffer +;; + +;; Flag and function to keep response buffer tidy. +(defvar pg-response-erase-flag nil + "Indicates that the response buffer should be cleared before next message.") + +(defun proof-shell-maybe-erase-response + (&optional erase-next-time clean-windows force) + "Erase the response buffer according to pg-response-erase-flag. +ERASE-NEXT-TIME is the new value for the flag. +If CLEAN-WINDOWS is set, use proof-clean-buffer to do the erasing. +If FORCE, override pg-response-erase-flag. + +If the user option proof-tidy-response is nil, then +the buffer is only cleared when FORCE is set. + +No effect if there is no response buffer currently. +Returns non-nil if response buffer was cleared." + (when (buffer-live-p proof-response-buffer) + (let ((doit (or (and + proof-tidy-response + (not (eq pg-response-erase-flag 'invisible)) + pg-response-erase-flag) + force))) + (if doit + (if clean-windows + (proof-clean-buffer proof-response-buffer) + ;; NB: useful optional arg to erase buffer is XEmacs specific, 8-(. + ;; (erase-buffer proof-response-buffer) + (with-current-buffer proof-response-buffer + (setq pg-response-next-error nil) ; all error msgs lost! + (erase-buffer) + (set-buffer-modified-p nil)))) + (setq pg-response-erase-flag erase-next-time) + doit))) + +(defun pg-response-display (str) + "Show STR as a response in the response buffer." + (unless pg-use-specials-for-fontify + (setq str (pg-assoc-strip-subterm-markup str))) +;;HERE changed t nil to t FORCE + (proof-shell-maybe-erase-response t nil) + ;;(unless (or (string-equal str "") (string-equal str "\n")) + ;; don't display an empty buffer [ NB: above test repeated below, + ;; but response-display reused elsewhere ] + + + (pg-response-display-with-face str) + ;; NB: this displays an empty buffer sometimes when it's not + ;; so useful. It _is_ useful if the user has requested to + ;; see the proof state and there is none + ;; (Isabelle/Isar displays nothing: might be better if it did). + (proof-display-and-keep-buffer proof-response-buffer)) + + +;; FIXME: this function should be combined with +;; proof-shell-maybe-erase-response-buffer. +(defun pg-response-display-with-face (str &optional face) + "Display STR with FACE in response buffer." + ;; 3.4: no longer return fontified STR, it wasn't used. + (cond + ((string-equal str "")) + ((string-equal str "\n")) ; quick exit, no display. + (t + (let (start end) + (with-current-buffer proof-response-buffer + ;; da: I've moved newline before the string itself, to match + ;; the other cases when messages are inserted and to cope + ;; with warnings after delayed output (non newline terminated). + (goto-char (point-max)) + ;; insert a newline before the new message unless the + ;; buffer is empty + (unless (eq (point-min) (point-max)) + (newline)) + (setq start (point)) + (insert str) + (unless (bolp) (newline)) + (proof-fontify-region start (point)) + ;; This is one reason why we don't keep the buffer in font-lock + ;; minor mode: it destroys this hacky property as soon as it's + ;; made! (Using the minor mode is much more convenient, tho') + (if (and face proof-output-fontify-enable) + (font-lock-append-text-property + start (point-max) 'face face)) + ;; This returns the decorated string, but it doesn't appear + ;; decorated in the minibuffer, unfortunately. + ;; [ FIXME: users have asked for that to be fixed ] + ;; 3.4: remove this for efficiency. + ;; (buffer-substring start (point-max)) + (set-buffer-modified-p nil)))))) + + +(defun pg-response-clear-displays () + "Clear Proof General response buffers. +You can use this command to clear the output from these buffers when +it becomes overly long. Particularly useful when `proof-tidy-response' +is set to nil, so responses are not cleared automatically." + (interactive) + (proof-map-buffers (list proof-response-buffer proof-trace-buffer proof-resolve-buffer) + (erase-buffer) + (set-buffer-modified-p nil))) + + + + + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; +;; Displaying in the resolution buffer +;; + +;; Flag and function to keep resolve buffer tidy. +(defvar pg-resolve-erase-flag nil + "Indicates that the resolve buffer should be cleared before next message.") + +(defun proof-shell-maybe-erase-resolve + (&optional erase-next-time clean-windows force) + "Erase the resolve buffer according to pg-resolve-erase-flag. +ERASE-NEXT-TIME is the new value for the flag. +If CLEAN-WINDOWS is set, use proof-clean-buffer to do the erasing. +If FORCE, override pg-resolve-erase-flag. + +If the user option proof-tidy-resolve is nil, then +the buffer is only cleared when FORCE is set. + +No effect if there is no resolve buffer currently. +Returns non-nil if resolve buffer was cleared." + (when (buffer-live-p proof-resolve-buffer) + (let ((doit (or (and + proof-tidy-resolve + (not (eq pg-resolve-erase-flag 'invisible)) + pg-resolve-erase-flag) + force))) + (if doit + (if clean-windows + (proof-clean-buffer proof-resolve-buffer) + ;; NB: useful optional arg to erase buffer is XEmacs specific, 8-(. + ;; (erase-buffer proof-resolve-buffer) + (with-current-buffer proof-resolve-buffer + (setq pg-resolve-next-error nil) ; all error msgs lost! + (erase-buffer) + (set-buffer-modified-p nil)))) + (setq pg-resolve-erase-flag erase-next-time) + doit))) + +(defun pg-resolve-display (str) + "Show STR as a resolve in the resolve buffer." + (unless pg-use-specials-for-fontify + (setq str (pg-assoc-strip-subterm-markup str))) + (proof-shell-maybe-erase-resolve t nil) + ;;(unless (or (string-equal str "") (string-equal str "\n")) + ;; don't display an empty buffer [ NB: above test repeated below, + ;; but resolve-display reused elsewhere ] + + + (pg-resolve-display-with-face str) + ;; NB: this displays an empty buffer sometimes when it's not + ;; so useful. It _is_ useful if the user has requested to + ;; see the proof state and there is none + ;; (Isabelle/Isar displays nothing: might be better if it did). + (proof-display-and-keep-buffer proof-resolve-buffer)) + + +;; FIXME: this function should be combined with +;; proof-shell-maybe-erase-resolve-buffer. +(defun pg-resolve-display-with-face (str &optional face) + "Display STR with FACE in resolve buffer." + ;; 3.4: no longer return fontified STR, it wasn't used. + (cond + ((string-equal str "")) + ((string-equal str "\n")) ; quick exit, no display. + (t + (let (start end) + (with-current-buffer proof-resolve-buffer + ;; da: I've moved newline before the string itself, to match + ;; the other cases when messages are inserted and to cope + ;; with warnings after delayed output (non newline terminated). + (goto-char (point-max)) + ;; insert a newline before the new message unless the + ;; buffer is empty + (unless (eq (point-min) (point-max)) + (newline)) + (setq start (point)) + (insert str) + (unless (bolp) (newline)) + (proof-fontify-region start (point)) + ;; This is one reason why we don't keep the buffer in font-lock + ;; minor mode: it destroys this hacky property as soon as it's + ;; made! (Using the minor mode is much more convenient, tho') + (if (and face proof-output-fontify-enable) + (font-lock-append-text-property + start (point-max) 'face face)) + ;; This returns the decorated string, but it doesn't appear + ;; decorated in the minibuffer, unfortunately. + ;; [ FIXME: users have asked for that to be fixed ] + ;; 3.4: remove this for efficiency. + ;; (buffer-substring start (point-max)) + (set-buffer-modified-p nil)))))) + + +(defun pg-resolve-clear-displays () + "Clear Proof General resolve buffer. +You can use this command to clear the output from these buffers when +it becomes overly long. Particularly useful when `proof-tidy-resolve' +is set to nil, so resolves are not cleared automatically." + (interactive) + (proof-map-buffers (list proof-resolve-buffer proof-trace-buffer proof-resolve-buffer) + (erase-buffer) + (set-buffer-modified-p nil))) + + + + + + |