From c564bc93d68696dd6b1dc44933e23c1d24656e94 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Sun, 24 Sep 2006 15:05:35 +0000 Subject: Add buffer history browsing --- CHANGES | 30 ++++- doc/ProofGeneral.texi | 10 ++ generic/pg-goals.el | 8 +- generic/pg-response.el | 9 +- generic/proof-autoloads.el | 52 +++++++- generic/proof-config.el | 9 ++ generic/proof-menu.el | 9 ++ generic/proof-utils.el | 3 +- lib/bufhist.el | 302 +++++++++++++++++++++++++++++++++++++++++++++ 9 files changed, 417 insertions(+), 15 deletions(-) create mode 100644 lib/bufhist.el 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 +;; 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-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) -- cgit v1.2.3