diff options
Diffstat (limited to 'generic/pg-response.el')
| -rw-r--r-- | generic/pg-response.el | 99 |
1 files changed, 99 insertions, 0 deletions
diff --git a/generic/pg-response.el b/generic/pg-response.el index 86dfe0ea..c1220a53 100644 --- a/generic/pg-response.el +++ b/generic/pg-response.el @@ -99,6 +99,105 @@ Internal variable, setting this will have no effect!") special-display-regexps))))) +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; +;; 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 proof-shell-next-error nil) ; all error msgs lost! + (erase-buffer)))) + (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-goals-strip-subterm-markup str))) + (proof-shell-maybe-erase-response t nil) + (pg-response-display-with-face str) + (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. + (if (string-equal str "\n") + str ; quick exit, no display. + (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). + ; (ugit (format "End is %i" (point-max))) + (goto-char (point-max)) + (newline) + (setq start (point)) + (insert str) + (unless (bolp) (newline)) + (setq end (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 end 'face face)) + ;; This returns the decorated string, but it doesn't appear + ;; decorated in the minibuffer, unfortunately. + ;; 3.4: remove this for efficiency. + ;; (buffer-substring start (point-max)) + )))) + + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; +;; Tracing buffers +;; + +;; An analogue of pg-response-display-with-face +(defun proof-trace-buffer-display (str) + "Display STR in the trace buffer." + (let (start end) + (with-current-buffer proof-trace-buffer + (goto-char (point-max)) + (newline) + (setq start (point)) + (insert str) + (unless (bolp) (newline)) + (proof-fontify-region start (point))))) + + (provide 'pg-response) |