diff options
author | Thomas Kleymann <da+pg-tms@inf.ed.ac.uk> | 1998-12-15 12:10:34 +0000 |
---|---|---|
committer | Thomas Kleymann <da+pg-tms@inf.ed.ac.uk> | 1998-12-15 12:10:34 +0000 |
commit | 3e9fc0816fc333ff80d158afa26bb70e403e6b1f (patch) | |
tree | 3ff9aaf8a4ee303893428e8a22d9e064fceb525a /generic/proof-toolbar.el | |
parent | e5a5aa225eb864da82c00870698d79befca977d8 (diff) |
made many minor changes to the documentation
Diffstat (limited to 'generic/proof-toolbar.el')
-rw-r--r-- | generic/proof-toolbar.el | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/generic/proof-toolbar.el b/generic/proof-toolbar.el index a89dc536..4a0c3e68 100644 --- a/generic/proof-toolbar.el +++ b/generic/proof-toolbar.el @@ -13,8 +13,11 @@ ;; Toolbar is just for scripting buffer at the moment. ;; + +;;; IMPORT declaration (require 'proof-script) (autoload 'proof-shell-live-buffer "proof-shell") +(autoload 'proof-shell-restart "proof-shell") (defconst proof-toolbar-default-button-list '(proof-toolbar-goal-button @@ -302,7 +305,7 @@ Move point if the end of the locked position is invisible." (progn (proof-toolbar-move (goto-char (proof-unprocessed-begin)) - (proof-assert-next-command)) + (proof-assert-next-command-interactive)) (proof-toolbar-follow)))) @@ -321,7 +324,7 @@ Move point if the end of the locked position is invisible." (progn (proof-toolbar-move (goto-char (point-min)) - (proof-retract-until-point)) ; gives error if process busy + (proof-retract-until-point-interactive)) ; gives error if process busy (proof-toolbar-follow)) (error "Nothing to retract in this buffer!"))) |