diff options
author | David Aspinall <da@inf.ed.ac.uk> | 1998-10-26 13:57:00 +0000 |
---|---|---|
committer | David Aspinall <da@inf.ed.ac.uk> | 1998-10-26 13:57:00 +0000 |
commit | 3675aca6bf99050ac1e61e71723b02fa08d6902b (patch) | |
tree | 22ff02bcf0115eb7a280fbc67278784d3a24d44e /generic/proof-toolbar.el | |
parent | 2ecf068cd43b41c11fde59a746cc4b9699458b33 (diff) |
proof-check-process-available replaced by *two* functions:
proof-activate-scripting
proof-shell-ready-prover
Diffstat (limited to 'generic/proof-toolbar.el')
-rw-r--r-- | generic/proof-toolbar.el | 14 |
1 files changed, 3 insertions, 11 deletions
diff --git a/generic/proof-toolbar.el b/generic/proof-toolbar.el index 2795ea18..f562ed14 100644 --- a/generic/proof-toolbar.el +++ b/generic/proof-toolbar.el @@ -200,16 +200,8 @@ Initialised in proof-toolbar-setup.") ;; GENERIC PROOF TOOLBAR FUNCTIONS ;; -(defun proof-toolbar-process-available-p () - "Enabler for toolbar functions. -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))) - (defun proof-toolbar-undo-enable-p () - (and (proof-toolbar-process-available-p) + (and (proof-shell-available-p) (> (proof-unprocessed-begin) (point-min)))) (defun proof-toolbar-undo () @@ -238,7 +230,7 @@ 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 () - (and (proof-toolbar-process-available-p) + (and (proof-shell-available-p) (member (current-buffer) proof-script-buffer-list))) (defun proof-toolbar-retract () @@ -282,7 +274,7 @@ Move point if the end of the locked position is invisible." (defun proof-toolbar-qed-enable-p () (and proof-shell-proof-completed - (proof-toolbar-process-available-p))) + (proof-shell-available-p))) (defun proof-toolbar-qed () "Insert a save theorem command into the script buffer, issue it." |