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-goals.el | |
parent | a744114658a01e46f16eec510e313b72da532aa0 (diff) |
Add buffer history browsing
Diffstat (limited to 'generic/pg-goals.el')
-rw-r--r-- | generic/pg-goals.el | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/generic/pg-goals.el b/generic/pg-goals.el index 59b65557..23bf522e 100644 --- a/generic/pg-goals.el +++ b/generic/pg-goals.el @@ -9,9 +9,10 @@ ;; ;; A sub-module of proof-shell; assumes proof-script loaded. - (require 'pg-assoc) +(require 'bufhist) + ;; Nuke some byte compiler warnings. (eval-when-compile (require 'easymenu)) @@ -40,6 +41,7 @@ May enable proof-by-pointing or similar features. (proof-toolbar-setup) (erase-buffer) (buffer-disable-undo) + (if proof-keep-response-history (bufhist-mode)) ; history for contents (set-buffer-modified-p nil))) ;; @@ -112,7 +114,9 @@ and properly fontifies STRING using proof-fontify-region." ;; Erase the goals buffer and add in the new string (set-buffer proof-goals-buffer) - (erase-buffer) + + (unless (eq 0 (buffer-size)) + (bufhist-checkpoint-and-erase)) ;; Only bother processing and displaying, etc, if string is ;; non-empty. (unless (string-equal string "") |