diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2006-09-24 15:05:35 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2006-09-24 15:05:35 +0000 |
| commit | c564bc93d68696dd6b1dc44933e23c1d24656e94 (patch) | |
| tree | c890d44e7944433bdfd2b7afedde3674e37f086e /generic/pg-response.el | |
| parent | a744114658a01e46f16eec510e313b72da532aa0 (diff) | |
Add buffer history browsing
Diffstat (limited to 'generic/pg-response.el')
| -rw-r--r-- | generic/pg-response.el | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/generic/pg-response.el b/generic/pg-response.el index c0f743df..ae010b19 100644 --- a/generic/pg-response.el +++ b/generic/pg-response.el @@ -10,10 +10,11 @@ ;; This mode is used for the response buffer proper, and ;; also the trace and theorems buffer. - ;; A sub-module of proof-shell; assumes proof-script loaded. (require 'pg-assoc) +(require 'bufhist) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; @@ -36,6 +37,7 @@ (setq pg-response-next-error nil) (erase-buffer) (buffer-disable-undo) + (if proof-keep-response-history (bufhist-mode)) ; history for contents (set-buffer-modified-p nil))) (easy-menu-define proof-response-mode-menu @@ -264,7 +266,7 @@ Returns non-nil if response buffer was cleared." ;; (erase-buffer proof-response-buffer) (with-current-buffer proof-response-buffer (setq pg-response-next-error nil) ; all error msgs lost! - (erase-buffer) + (bufhist-checkpoint-and-erase) (set-buffer-modified-p nil)))) (setq pg-response-erase-flag erase-next-time) doit))) @@ -328,7 +330,8 @@ 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) - (erase-buffer) + (if (> (buffer-size) 0) + (bufhist-checkpoint-and-erase)) (set-buffer-modified-p nil))) |