diff options
| author |  Thomas Kleymann <da+pg-tms@inf.ed.ac.uk> | 1998-10-21 11:50:23 +0000 |
|---|---|---|
| committer | Thomas Kleymann <da+pg-tms@inf.ed.ac.uk> | 1998-10-21 11:50:23 +0000 |
| commit | 6d2cf60d7e3920c712b9599994483571a5ac56b1 (patch) | |
| tree | b3e8233050702cdd321925a9689911b6dc4e27ff /generic/proof-toolbar.el | |
| parent | f2af9565265997004c0906b7a0c68efad44ce5cf (diff) | |
o Improved error messages
o Fixed bug in proof-toolbar-next
Diffstat (limited to 'generic/proof-toolbar.el')
| -rw-r--r-- | generic/proof-toolbar.el | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/generic/proof-toolbar.el b/generic/proof-toolbar.el index ad8928b0..31a70e9d 100644 --- a/generic/proof-toolbar.el +++ b/generic/proof-toolbar.el @@ -208,14 +208,15 @@ without giving error messages." (defun proof-toolbar-undo-enable-p () (and (proof-toolbar-process-available-p) - (proof-locked-end))) + (> (proof-unprocessed-begin) (point-min)))) (defun proof-toolbar-undo () "Undo last successful in locked region, without deleting it." (interactive) (if (proof-toolbar-undo-enable-p) (save-excursion - (proof-undo-last-successful-command t)))) + (proof-undo-last-successful-command t)) + (error "I don't know what I should undo in this buffer!"))) (defun proof-toolbar-next-enable-p () ;; Could check if there *is* a next command here, to avoid @@ -228,7 +229,7 @@ Move point if the end of the locked position is invisible." (interactive) (save-excursion (if (proof-shell-live-buffer) - (goto-char (proof-locked-end)) + (goto-char (proof-unprocessed-begin)) (goto-char (point-min))) (proof-assert-next-command)) ;; FIXME: not sure about whether this is nice or not. |