diff options
| -rw-r--r-- | etc/README | 3 | ||||
| -rw-r--r-- | generic/proof-shell.el | 5 | ||||
| -rw-r--r-- | generic/proof.el | 35 | ||||
| -rw-r--r-- | todo | 4 |
4 files changed, 30 insertions, 17 deletions
@@ -10,3 +10,6 @@ lego Files for testing LEGO Proof General isa Files for testing Isabelle Proof General +README this file + +example test protocol for example proof script
\ No newline at end of file diff --git a/generic/proof-shell.el b/generic/proof-shell.el index b2e6dd30..da88bf30 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -363,6 +363,9 @@ This is a list of tuples of the form (type . string). type is either (incf ip)) (set-buffer proof-pbp-buffer) (erase-buffer) + ;; Perhaps we ought to erase the proof-response-buffer at this + ;; point as well. It may contain an error message referring to + ;; an *earlier* state in the proof. (insert (substring out 0 op)) (proof-display-and-keep-buffer proof-pbp-buffer) @@ -491,6 +494,8 @@ we call `proof-shell-handle-error-hook'. " (cdr proof-shell-delayed-output))) (proof-display-and-keep-buffer proof-pbp-buffer))) + ;; Perhaps we should erase the buffer in proof-response-buffer, too? + ;; We extract all text between text matching ;; `proof-shell-error-regexp' and the following prompt. ;; Alternatively one could higlight all output between the diff --git a/generic/proof.el b/generic/proof.el index 440c2ab8..ef3e68a6 100644 --- a/generic/proof.el +++ b/generic/proof.el @@ -151,21 +151,26 @@ The argument KBL is a list of tuples (k . f) where `k' is a keybinding (defun proof-display-and-keep-buffer (buffer) - "Display BUFFER and mark window according to `proof-window-dedicated-p'." - (let ((window (get-buffer-window buffer 'visible))) - (save-selected-window - (save-excursion - (display-buffer buffer) - (set-window-dedicated-p (get-buffer-window buffer) - proof-window-dedicated-p) - (and window - (progn (select-window window) - ;; tms: I don't understand why the point in - ;; proof-response-buffer is not at the end anyway. - ;; Is there a superfluous save-excursion somewhere? - (set-buffer buffer) - (goto-char (point-max)) - (or (pos-visible-in-window-p) (recenter -1)))))))) + "Display BUFFER and mark window according to `proof-window-dedicated-p'. + +Also ensures that point is visible." + (let (window) + (save-excursion + (set-buffer buffer) + (display-buffer buffer) + (setq window (get-buffer-window buffer 'visible)) + (set-window-dedicated-p window proof-window-dedicated-p) + (and window + (save-selected-window + (select-window window) + + ;; tms: I don't understand why the point in + ;; proof-response-buffer is not at the end anyway. + ;; Is there a superfluous save-excursion somewhere? + (goto-char (point-max)) + + (or (pos-visible-in-window-p (point) window) + (recenter -1))))))) (defun proof-clean-buffer (buffer) "Erase buffer and hide from display." @@ -14,8 +14,6 @@ X (Low) probably not worth wasting time on * This is a list of things which need doing in the generic interface ==================================================================== -A* Fix display handling problems (tms, all week) - A* multiple files bug fix: It can happen (in Isabelle) that the prover retracts a file which asks for another to be retracted which is *not* on @@ -73,6 +71,8 @@ C Remove "FIXME notes" which are just notes I've put in about old C Check on all FIXME notes. +C automise testing procedures in etc/ + C Write proof-define-derived-mode which automatically adds a call back hook somehow. Propose this to maintainer of derived.el. (1.5hrs) |