aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic/pg-goals.el
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2006-09-24 15:05:35 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2006-09-24 15:05:35 +0000
commitc564bc93d68696dd6b1dc44933e23c1d24656e94 (patch)
treec890d44e7944433bdfd2b7afedde3674e37f086e /generic/pg-goals.el
parenta744114658a01e46f16eec510e313b72da532aa0 (diff)
Add buffer history browsing
Diffstat (limited to 'generic/pg-goals.el')
-rw-r--r--generic/pg-goals.el8
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 "")