Add buffer history browsing

9 files changed, 417 insertions, 15 deletions

diff --git a/CHANGES b/CHANGES
index 78356075..d9a7ee47 100644
--- a/CHANGES
+++ b/CHANGES
@@ -4,6 +4,21 @@ See also etc/release-log.txt for minor patches.
 
 * Summary of Changes for Proof General 3.6 from 3.5
 
+** Generic changes
+
+*** History mechanism for prover responses
+
+Proof General will keep a history of the last 10 responses from the
+prover in each of the buffers used to display messages.  This is handy
+for examining previous proof state outputs without actually issuing
+undo/redo commands to the prover, for example.  Of for browsing
+previous displays of theorems or rules.
+
+To use this, enable Proof General -> Option -> Response History.
+
+Then the keys M-left, M-right will browse the history in
+each buffer.  See "C-h m" for more documentation.
+
 *** Large X-Symbol fonts added, courtesy of Clemens Ballarin
 
 May use option -f 18 or -f 24 of the Isabelle interface wrapper.
@@ -13,9 +28,13 @@ May use option -f 18 or -f 24 of the Isabelle interface wrapper.
 See proof-shell-unicode (default nil), or option -U of the Isabelle
 interface wrapper.
 
-*** Improved compatibility with Coq 8
+*** Minor fixes and tweaks
+
+Including numerous improvements from Stefan Monnier.
+
 
-Several fixes.  Also, removed support for Coq 6, 7.
+
+** Changes for Isabelle
 
 *** Support for Isabelle2005 and current development version of Isabelle.  
 
@@ -27,10 +46,6 @@ Isabelle2004 should still be functional with this version of Proof
 General.  Support for Isabelle 2003 has been removed.
 
 
-*** Miscellaneous fixes
-
-Including numerous improvements from Stefan Monnier.
-
 
 ** Changes for Coq
 
@@ -110,6 +125,9 @@ Including numerous improvements from Stefan Monnier.
 *** new "queries" menu
 
 
+
+
+
 * Summary of Changes for Proof General 3.5 from 3.4
 
 ** Generic changes
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 8c78919a..bb1a7d8d 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -2833,6 +2833,16 @@ Otherwise the response buffer will accumulate output from the prover.
 The default value is @code{t}.
 @end defopt
 
+@c TEXI DOCSTRING MAGIC: proof-keep-response-history
+@defopt proof-keep-response-history
+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).
+
+The default value is @code{nil}.
+@end defopt
+
 @c TEXI DOCSTRING MAGIC: proof-show-debug-messages
 @defopt proof-show-debug-messages 
 Whether to display debugging messages in the response buffer.@*
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!
diff --git a/lib/bufhist.el b/lib/bufhist.el
new file mode 100644
index 00000000..83981251
--- /dev/null
+++ b/lib/bufhist.el
@@ -0,0 +1,302 @@
+;; bufhist.el --- keep read-only history of buffer contents for browsing
+
+;; Copyright   (C) 2006 David Aspinall / University of Edinburgh
+
+;; Author:     David Aspinall <David.Aspinall@ed.ac.uk>
+;; License:    GPL (GNU GENERAL PUBLIC LICENSE)
+;; Keywords:   tools
+;;
+;; $Id$ 
+;;
+;; This file is distributed under the terms of the GNU General Public
+;; License, Version 2.  Find a copy of the GPL with your version of
+;; GNU Emacs or Texinfo.
+;; 
+;; This library implements a minor mode for which keeps a ring history of
+;; buffer contents.  Intended to be used for small buffers which are 
+;; intermittently updated (e.g. status panels/displays), for which history
+;; browsing is useful.
+;;
+
+;; TODO: a more PG-specific and efficient approach would be to keep
+;; regions within a single buffer rather than copying strings in and out.
+;; That way we could use cloned (indirect) buffers which allow independent
+;; browsing of the history.
+;;
+;; FIXME: autoloading this doesn't work too well.  
+;; Advice on erase-buffer doesn't work. 
+
+;;; First a function which ought to be in ring.el
+
+(defun bufhist-ring-update (ring index newitem)
+  "Update RING at position INDEX with NEWITEM."
+  (if (ring-empty-p ring)
+      (error "Accessing an empty ring")
+    (let* ((hd (car ring))  (ln (car (cdr ring)))  (vec (cdr (cdr ring))))
+      (aset vec (ring-index index hd ln (length vec)) newitem))))
+
+;;; Now our code
+
+(defgroup bufhist nil
+  "In-memory history of buffer contents"
+  :group 'tools)
+
+(defcustom bufhist-ring-size 10
+  "*Default size of buffer history ring."
+  :group 'bufhist
+  :type 'integer)
+
+(defvar bufhist-ring nil
+  "Ring history of buffer.  Always non-empty.")
+
+(defvar bufhist-ring-pos nil
+  "Current position in ring history of buffer.")
+
+(defvar bufhist-lastswitch-modified-tick nil
+  "Value of (buffer-modified-tick) at last switch buffer.")
+
+(defvar bufhist-read-only-history t
+  "Whether history is editable.")
+
+(defvar bufhist-saved-mode-line-format nil
+  "Ordinary value of mode-line-format for this buffer.")
+
+(defconst bufhist-mode-line-format-entry
+  '(" [hist:" 
+    (:eval (int-to-string (- (ring-length bufhist-ring)
+			     bufhist-ring-pos))) "/" 
+    (:eval (int-to-string (ring-length bufhist-ring))) "]"))
+
+(make-variable-buffer-local 'bufhist-ring)
+(make-variable-buffer-local 'bufhist-ring-pos)
+(make-variable-buffer-local 'bufhist-lastswitch-modified-tick)
+(make-variable-buffer-local 'bufhist-read-only-history)
+
+(defun bufhist-get-buffer-contents ()
+  "Return the stored representation of the current buffer contents."
+  ;; First: make all extents in the buffer duplicable to recreate them
+  (if (fboundp 'mapcar-extents)
+      (mapcar-extents (lambda (ext) 
+			(set-extent-property ext 'duplicable t))))
+  (cons (point)
+	(buffer-substring (point-max) (point-min))))
+
+(fset 'bufhist-ordinary-erase-buffer (symbol-function 'erase-buffer))
+;(defalias 'bufhist-ordinary-erase-buffer 'erase-buffer)
+
+(defun bufhist-restore-buffer-contents (buf)
+  "Restore BUF as the contents of the current buffer."
+  (bufhist-ordinary-erase-buffer)
+  (insert (cdr buf))
+  ;; don't count this as a buffer update
+  (setq bufhist-lastswitch-modified-tick (buffer-modified-tick))
+  (goto-char (car buf)))
+
+(defun bufhist-checkpoint ()
+  "Add buffer contents to the ring history.  No action if not in bufhist mode."
+  (interactive)
+  (if bufhist-mode ;; safety
+      (ring-insert bufhist-ring (bufhist-get-buffer-contents))))
+
+(defun bufhist-erase-buffer ()
+  "Erase buffer contents, maybe running bufhist-before-change-function first."
+  ;; Unfortunately on XEmacs, erase-buffer doesn't call
+  ;; before-change-functions (it does on GNU Emacs)
+  ;; This would be easier with advice 
+  (if (and 
+       bufhist-mode
+       (string-match "XEmacs" emacs-version)
+       (memq 'bufhist-before-change-function before-change-functions))
+      (let ((before-change-functions nil)
+	    (after-change-functions nil))
+	(bufhist-before-change-function)))
+  (erase-buffer))
+
+(defun bufhist-checkpoint-and-erase ()
+  "Add buffer contents to history then erase. Only erase if not in bufhist mode"
+  (interactive)
+  (bufhist-checkpoint)
+  (bufhist-erase-buffer))
+
+(defun bufhist-switch-to-index (n &optional nosave browsing)
+  "Switch to position N in buffer history, maybe updating history.
+If optional NOSAVE is non-nil, do not try to save current contents."
+  (if browsing
+      (message "History position %d of %d" 
+	       (- (ring-length bufhist-ring) n)
+	       (ring-length bufhist-ring)))
+  (unless (equal n bufhist-ring-pos) 
+    ;; we're moving to different position
+    (let ((tick (buffer-modified-tick)))
+      ;; Save changes back to history for most recent contents or for
+      ;; older contents if we have read-write history
+      (unless (or nosave
+		  (and bufhist-read-only-history (not (eq bufhist-ring-pos 0)))
+		  (equal tick bufhist-lastswitch-modified-tick))
+	;; If we're browsing away from position 0, checkpoint instead
+	;; of updating.
+	;; NB: logic here should ideally keep flag to say whether 
+	;; changes are "during" a browse or not.  This is going
+	;; to result in too many checkpoints if we have manual
+	;; editing.
+	(if (and browsing (eq bufhist-ring-pos 0))
+	    ;(progn
+	    (bufhist-checkpoint)
+	  ; (setq n (1+ n)))
+	  ;; Otherwise update in-position
+	  (bufhist-ring-update bufhist-ring bufhist-ring-pos 
+			       (bufhist-get-buffer-contents))))
+      (setq bufhist-lastswitch-modified-tick tick)
+      (let ((before-change-functions nil)
+	    (buffer-read-only nil))
+	(bufhist-restore-buffer-contents (ring-ref bufhist-ring n)))
+      (if bufhist-read-only-history
+	  (setq buffer-read-only 
+		(if (eq n 0) bufhist-normal-read-only t)))
+      (setq bufhist-ring-pos n)
+      (force-mode-line-update))))
+
+(defun bufhist-first ()
+  "Switch to most oldest buffer contents."
+  (interactive)
+  (bufhist-switch-to-index (1- (ring-length bufhist-ring)) nil 'browsing))
+
+(defun bufhist-last ()
+  "Switch to last (most recent; current) buffer contents."
+  (interactive)
+  (bufhist-switch-to-index 0 nil 'browsing))
+  
+(defun bufhist-prev (&optional n)
+  "Browse backward in the history of buffer contents."
+  (interactive "p")
+  (bufhist-switch-to-index
+   (mod (+ bufhist-ring-pos (or n 1))
+	(ring-length bufhist-ring))
+   nil 'browsing))
+
+(defun bufhist-next (&optional n)
+  "Browse forward in the history of buffer contents."
+  (interactive "p")
+  (bufhist-prev (- (or n 1))))
+
+(defun bufhist-delete ()
+  "Delete the current item in the buffer history."
+  (interactive)
+  (unless (eq 0 bufhist-ring-pos)
+    (ring-remove bufhist-ring bufhist-ring-pos)
+    (bufhist-switch-to-index (1- bufhist-ring-pos) 'nosave)))
+
+;; FIXME: bug here, we get duplicated first item after clear
+(defun bufhist-clear ()
+  "Clear history."
+  (interactive)
+  (bufhist-switch-to-index 0 'nosave) 
+  (setq bufhist-ring (make-ring (ring-size bufhist-ring)))
+  (setq bufhist-ring-pos 0)
+  (bufhist-checkpoint)
+  (setq bufhist-lastswitch-modified-tick (buffer-modified-tick)))
+
+
+;; Setup functions
+
+(defun bufhist-init (&optional readwrite ringsize)
+  "Initialise a ring history for the current buffer.
+The history will be read-only unless READWRITE is non-nil.
+For read-only histories, edits to the buffer switch to the latest version.
+The size defaults to `bufhist-ring-size'."
+  (interactive)
+  (setq bufhist-ring (make-ring (or ringsize bufhist-ring-size)))
+  (setq bufhist-normal-read-only buffer-read-only)
+  (setq bufhist-read-only-history (not readwrite))
+  (setq bufhist-ring-pos 0)
+  (setq bufhist-saved-mode-line-format mode-line-format)
+  (bufhist-checkpoint)
+  (setq mode-line-format 
+	(cons (cons 'bufhist-mode (list bufhist-mode-line-format-entry))
+	      ;; surely it's always a list, but in case not
+	      (if (listp mode-line-format) 
+		  mode-line-format 
+		(list mode-line-format))))
+  (force-mode-line-update)
+  (make-local-variable 'before-change-functions)
+  (bufhist-set-readwrite readwrite))
+
+
+(defun bufhist-exit ()
+  "Stop keeping ring history for current buffer."
+  (interactive)
+  (bufhist-switch-to-index 0)
+  (bufhist-set-readwrite t)
+  (setq mode-line-format bufhist-saved-mode-line-format)
+  (force-mode-line-update))
+
+
+
+
+(defun bufhist-set-readwrite (readwrite)
+  "Set `before-change-functions' for read-only history."
+  (if readwrite
+      ;; edit directly
+      (progn
+	(setq before-change-functions
+	      (remq 'bufhist-before-change-function before-change-functions)))
+;	(if (string-match "XEmacs" emacs-version)
+;	    (ad-disable-advice 'erase-buffer 'before 'bufhist-last-advice)))
+    ;; readonly history: switch to latest contents
+    (setq before-change-functions
+	  (cons 'bufhist-before-change-function before-change-functions))))
+;	(if (string-match "XEmacs" emacs-version)
+;	    (ad-enable-advice 'erase-buffer 'before 'bufhist-last-advice))))
+
+;; Restore the latest buffer contents before changes from elsewhere.
+
+(defun bufhist-before-change-function (&rest args)
+  "Restore the most recent contents of the buffer before changes."
+  (bufhist-switch-to-index 0))
+
+;; On XEmacs, erase-buffer does not call before-change-function
+;(if (string-match "XEmacs" emacs-version)
+;    (progn
+;      (defadvice erase-buffer (before bufhist-last-advice activate)
+;	(if (and bufhist-mode bufhist-read-only-history)
+;	    (bufhist-last)))
+;      (ad-activate-on 'erase-buffer)))
+
+
+;;; Minor mode 
+
+;;;###autoload
+(autoload 'bufhist-mode "bufhist"
+  "Minor mode retaining an in-memory history of the buffer contents.")
+
+(defconst bufhist-minor-mode-map
+  (let ((map (make-sparse-keymap)))
+    ;; (define-key map [mouse-2] 'bufhist-popup-menu)
+    (define-key map [(meta left)] 'bufhist-prev)
+    (define-key map [(meta right)] 'bufhist-next)
+    (define-key map [(meta up)] 'bufhist-first)
+    (define-key map [(meta down)] 'bufhist-last)
+    (define-key map [(meta c)] 'bufhist-clear)
+    (define-key map [(meta d)] 'bufhist-delete)
+    map)
+  "Keymap for `bufhist-minor-mode'.")
+
+(define-minor-mode bufhist-mode
+  "Minor mode retaining an in-memory history of the buffer contents.
+
+Commands:\\<bufhist-minor-mode-map>
+\\[bufhist-prev]    bufhist-prev    go back in history  
+\\[bufhist-next]    bufhist-next    go forward in history  
+\\[bufhist-first]   bufhist-first   go to first item in history
+\\[bufhist-last]    bufhist-last    go to last (current) item in history.
+\\[bufhist-clear]   bufhist-clear   clear history.
+\\[bufhist-delete]  bufhist-clear   delete current item from history."
+  nil "" bufhist-minor-mode-map
+  :group 'bufhist
+  (if bufhist-mode 
+      (bufhist-init)
+    (bufhist-exit)))
+
+
+
+(provide 'bufhist)