6 files changed, 81 insertions, 9 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 "")
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)))
 
 
diff --git a/generic/proof-autoloads.el b/generic/proof-autoloads.el
index b828a997..907590ed 100644
--- a/generic/proof-autoloads.el
+++ b/generic/proof-autoloads.el
@@ -56,11 +56,15 @@ All of these settings are optional." nil 'macro)
 
 ;;;***
 
-;;;### (autoloads (proof-define-assistant-command-witharg) "pg-user" "generic/pg-user.el")
+;;;### (autoloads (proof-define-assistant-command-witharg proof-define-assistant-command) "pg-user" "generic/pg-user.el")
+
+(autoload 'proof-define-assistant-command "pg-user" "\
+Define command FN to send string BODY to proof assistant, based on CMDVAR.
+BODY defaults to CMDVAR, a variable." nil 'macro)
 
 (autoload 'proof-define-assistant-command-witharg "pg-user" "\
 Define command FN to prompt for string CMDVAR to proof assistant.
-CMDVAR is a function or string.  Automatically has history." nil 'macro)
+CMDVAR is a variable holding a function or string.  Automatically has history." nil 'macro)
 
 ;;;***
 
@@ -226,7 +230,7 @@ may be a string or sexp evaluated to get a string." nil nil)
 
 (autoload 'proof-toolbar-setup "proof-toolbar" "\
 Initialize Proof General toolbar and enable it for current buffer.
-If proof-mode-use-toolbar is nil, change the current buffer toolbar
+If `proof-toolbar-enable' is nil, change the current buffer toolbar
 to the default toolbar." t nil)
 
 ;;;***
@@ -253,4 +257,46 @@ Assumes that the current buffer is the proof shell buffer." nil nil)
 Configure the current output buffer (goals/response/trace) for X-Symbol." nil nil)
 
 ;;;***
+
+;;;### (autoloads (bufhist-checkpoint) "bufhist" "lib/bufhist.el")
+
+(autoload 'bufhist-checkpoint "bufhist" "\
+Add the current buffer contents to the ring history." t nil)
+
+(autoload 'bufhist-mode "bufhist" "\
+Minor mode retaining an in-memory history of the buffer contents.")
+
+;;;***
+
+;;;### (autoloads nil "bufregring" "lib/bufregring.el")
+
+(autoload 'bufhist-mode "bufhist" "\
+Minor mode retaining an in-memory history of the buffer contents.")
+
+;;;***
+
+;;;### (autoloads nil "bufregs" "lib/bufregs.el")
+
+(autoload 'bufregs-mode "bufregs" "\
+Minor mode retaining an in-memory history of the buffer contents.")
+
+;;;***
+
+;;;### (autoloads (holes-mode) "holes" "lib/holes.el")
+
+(autoload 'holes-mode "holes" "\
+If ARG is nil, then toggle holes mode on/off.
+If arg is positive, then turn holes mode on.  If arg is negative, then
+turn it off." t nil)
+
+;;;***
+
+;;;### (autoloads (texi-docstring-magic) "texi-docstring-magic" "lib/texi-docstring-magic.el")
+
+(autoload 'texi-docstring-magic "texi-docstring-magic" "\
+Update all texi docstring magic annotations in buffer.
+With prefix arg, no errors on unknown symbols.  (This results in
+@def .. @end being deleted if not known)." t nil)
+
+;;;***
 
diff --git a/generic/proof-config.el b/generic/proof-config.el
index 09c32a7d..4dd81147 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -303,6 +303,15 @@ Otherwise the response buffer will accumulate output from the prover."
   :type 'boolean
   :group 'proof-user-options)
 
+(defcustom proof-keep-response-history
+  nil
+  "*Whether to keep a browsable history of responses.
+With this feature enabled, the buffers used for prover responses will have a
+history that can be browsed without processing/undoing in the prover.
+(Changes to this variable take effect after restarting the prover)."
+  :type 'boolean
+  :group 'proof-user-options)
+
 (defcustom proof-show-debug-messages nil
   "*Whether to display debugging messages in the response buffer.
 If non-nil, debugging messages are displayed in the response giving
diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index 31b1c965..0a7533a6 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -270,6 +270,9 @@ without adjusting window layout."
 (proof-deftoggle-fn (proof-ass-sym x-symbol-enable) 'proof-x-symbol-toggle)
 (proof-deftoggle-fn (proof-ass-sym mmm-enable) 'proof-mmm-toggle)
 
+;; TODO (low priority): add dynamic enable-disable
+(proof-deftoggle proof-keep-response-history)
+
 ;; Here is the menu
 
 (defconst proof-quick-opts-menu
@@ -317,6 +320,11 @@ without adjusting window layout."
 			 (eq proof-buffer-type 'script))
       :style toggle
       :selected proof-toolbar-enable]
+
+     ["Response history" proof-keep-response-history-toggle
+      :style toggle
+      :selected proof-keep-response-history]
+
      ["Index Menu" proof-imenu-toggle
       :active (stringp (locate-library "imenu"))
       :style toggle
@@ -391,6 +399,7 @@ without adjusting window layout."
    (proof-ass-sym x-symbol-enable)
    (proof-ass-sym mmm-enable)
    'proof-toolbar-enable
+   'proof-keep-response-history
    'proof-imenu-enable
    ;; Display sub-menu
    'proof-three-window-enable
diff --git a/generic/proof-utils.el b/generic/proof-utils.el
index 280de2d6..887d2b95 100644
--- a/generic/proof-utils.el
+++ b/generic/proof-utils.el
@@ -571,7 +571,8 @@ frame is the one showing the script buffer.)
 No effect if buffer is dead."
   (if (buffer-live-p buffer)
       (with-current-buffer buffer
-	(erase-buffer)
+	(unless (eq 0 (buffer-size)) ;; checkpoint unless already empty
+	  (bufhist-checkpoint-and-erase))
 	(set-buffer-modified-p nil)
 	(if (eq buffer proof-response-buffer)
 	    (setq pg-response-next-error nil))	; all error msgs lost!