aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic/proof-toolbar.el
diff options
context:
space:
mode:
authorGravatar Thomas Kleymann <da+pg-tms@inf.ed.ac.uk>1998-12-15 12:10:34 +0000
committerGravatar Thomas Kleymann <da+pg-tms@inf.ed.ac.uk>1998-12-15 12:10:34 +0000
commit3e9fc0816fc333ff80d158afa26bb70e403e6b1f (patch)
tree3ff9aaf8a4ee303893428e8a22d9e064fceb525a /generic/proof-toolbar.el
parente5a5aa225eb864da82c00870698d79befca977d8 (diff)
made many minor changes to the documentation
Diffstat (limited to 'generic/proof-toolbar.el')
-rw-r--r--generic/proof-toolbar.el7
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!")))