diff options
| author |  Thomas Kleymann <da+pg-tms@inf.ed.ac.uk> | 1998-10-18 14:18:26 +0000 |
|---|---|---|
| committer | Thomas Kleymann <da+pg-tms@inf.ed.ac.uk> | 1998-10-18 14:18:26 +0000 |
| commit | bb0b35e13e222ceffee83d49ec676c8b88c51966 (patch) | |
| tree | 1929a06b10b381177b030e9a3f983f437e2fabe6 /generic/proof-toolbar.el | |
| parent | d6501c39e4975a1b34b145a21602b9fb99202e3d (diff) | |
relaxed conditions in light of new multiple files support
Diffstat (limited to 'generic/proof-toolbar.el')
| -rw-r--r-- | generic/proof-toolbar.el | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/generic/proof-toolbar.el b/generic/proof-toolbar.el index 916ba661..ad8928b0 100644 --- a/generic/proof-toolbar.el +++ b/generic/proof-toolbar.el @@ -204,9 +204,7 @@ Checks based on those in proof-check-process-available, but without giving error messages." (and (eq proof-buffer-type 'script) (proof-shell-live-buffer) - (not proof-shell-busy) - ;; this last check is wrong for pbp buffer! - (eq (car proof-script-buffer-list) (current-buffer)))) + (not proof-shell-busy))) (defun proof-toolbar-undo-enable-p () (and (proof-toolbar-process-available-p) @@ -237,7 +235,8 @@ Move point if the end of the locked position is invisible." (proof-goto-end-of-locked-if-pos-not-visible-in-window)) (defun proof-toolbar-retract-enable-p () - (proof-toolbar-process-available-p)) + (and (proof-toolbar-process-available-p) + (member (current-buffer) proof-script-buffer-list))) (defun proof-toolbar-retract () "Retract buffer." |