From 7ae642f20e2c0656444bf116202f7b5f1d2bca94 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Mon, 12 Oct 1998 15:52:33 +0000
Subject: Made toolbar functions interactive, needed by old XEmacs.

---
 generic/proof-toolbar.el | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/generic/proof-toolbar.el b/generic/proof-toolbar.el
index 15a64fbe..de867fc5 100644
--- a/generic/proof-toolbar.el
+++ b/generic/proof-toolbar.el
@@ -226,6 +226,7 @@ without giving error messages."
 (defun proof-toolbar-next ()
   "Assert next command in proof to proof process.
 Move point if the end of the locked position is invisible."
+  (interactive)
   (save-excursion
     (if (proof-shell-live-buffer)
       (goto-char (proof-locked-end))
@@ -240,6 +241,7 @@ Move point if the end of the locked position is invisible."
 (defun proof-toolbar-retract ()
   "Retract buffer."
   ;; proof-retract-file might be better here!
+  (interactive)
   (if (proof-toolbar-retract-enable-p)
       (save-excursion
 	(goto-char (point-min))
@@ -252,6 +254,7 @@ Move point if the end of the locked position is invisible."
 
 (defun proof-toolbar-use 
   "Process the whole buffer"
+  (interactive)
   (save-excursion
     (proof-process-buffer)))
 
@@ -261,6 +264,7 @@ Move point if the end of the locked position is invisible."
   (eq proof-buffer-type 'script))
 
 (defun proof-toolbar-restart  ()
+  (interactive)
   (if (proof-toolbar-restart-enable-p)
       ((if (yes-or-no-p (concat "Restart " proof-assistant " scripting?"))
 	   (proof-restart-script)))))
@@ -278,6 +282,8 @@ Move point if the end of the locked position is invisible."
        (proof-toolbar-process-available-p)))
 
 (defun proof-toolbar-qed 
+  "Insert a save theorem command into the script buffer, issue it."
+  (interactive)
   (if (proof-toolbar-qed-enable-p)
       (proof-issue-save)))
 ;; 
-- 
cgit v1.2.3