Added new toolbar buttons, streamlined code to work from a table

1 files changed, 168 insertions, 152 deletions

diff --git a/generic/proof-toolbar.el b/generic/proof-toolbar.el
index c7d741dc..bccc6eb0 100644
--- a/generic/proof-toolbar.el
+++ b/generic/proof-toolbar.el
@@ -10,8 +10,28 @@
 ;; proof-toolbar-menu which holds the same commands and is put on the
 ;; menubar by proof-toolbar-setup (surprisingly).
 ;;
-;; Toolbar is just for scripting buffer at  the moment.
+;; Toolbar is just for the scripting buffer currently.
 ;;
+;;
+;; TODO:
+;;
+;; FIXME: edit-toolbar cannot edit proof toolbar (even in a proof mode)
+;; Need a variable containing  a specifier or similar.
+;; (defvar proof-toolbar-specifier nil
+;;   "Specifier for proof toolbar.")
+;; This doesn't seem worth fixing until XEmacs toolbar implementation
+;; settles a bit.  Enablers don't work too well at the moment.
+
+;; FIXME: it's a little bit tricky to add prover-specific items.
+;; We can improve on that by generating everything on-thy-fly
+;; in proof-toolbar-setup.
+
+;; FIXME: In the future, add back the enabler functions.
+;; As of 20.4, they *almost* work, but it seems difficult
+;; to get the toolbar to update at the right times.
+;; For older versions of XEmacs (19.15, P.C.Callaghan@durham.ac.uk
+;; reports) the toolbar specifier format doesn't like
+;; arbitrary sexps as the enabler, either.
 
 
 ;;; IMPORT declaration 
@@ -19,49 +39,74 @@
 (autoload 'proof-shell-live-buffer "proof-shell")
 (autoload 'proof-shell-restart "proof-shell")
 
-(defconst proof-toolbar-default-button-list
-  '(proof-toolbar-goal-button
-    proof-toolbar-retract-button
-    proof-toolbar-undo-button
-    proof-toolbar-next-button
-    proof-toolbar-use-button
-    proof-toolbar-restart-button
-    proof-toolbar-qed-button
-    '[:style 3d]
-    nil)
-  "Example value for proof-toolbar-button-list.
+
+;;
+;; The default generic toolbar
+;;
+(defconst proof-toolbar-entries-default
+  '((show	"Show"		"Show the current proof state" t)
+    (context	"Context"	"Show the current context" t)
+    (goal	"Goal"		"Start a new proof" t)
+    (retract	"Retract"	"Retract (undo) whole buffer" t)
+    (undo	"Undo"		"Undo the previous proof command" t)
+    (next	"Next"		"Process the next proof command" t)
+    (use	"Use"		"Process whole buffer" t)
+    (restart	"Restart"	"Restart scripting (clear all locked regions)" t)
+    (qed	"QED"		"Close/save proved theorem" t)
+    (command    "Command"	"Issue a non-scripting command")
+    (info	"Info"		"Show proof assistant information" t))
+"Example value for proof-toolbar-entries.
 This gives a bare toolbar that works for any prover.  To add
-prover specific buttons, see proof-toolbar.el.")
+prover specific buttons, see documentation for proof-toolbar-entries
+and the file proof-toolbar.el.")
+
+(defvar proof-toolbar-entries
+  proof-toolbar-entries-default
+  "List of entries for Proof General toolbar.
+Format of each entry is (TOKEN MENUNAME TOOLBARTEXT ENABLER-P).
+For each TOKEN, we expect an icon with base filename TOKEN,
+		          a function proof-toolbar-<TOKEN>,
+         and (optionally) an enabler proof-toolbar-<TOKEN>-enable-p.")
+
+
+;;
+;; Function, icon, button names
+;; 
+
+(defun proof-toolbar-function (token)
+  (intern (concat "proof-toolbar-" (symbol-name token))))
+
+(defun proof-toolbar-icon (token)
+  (intern (concat "proof-toolbar-" (symbol-name token) "-icon")))
+
+(defun proof-toolbar-enabler (token)
+  (intern (concat "proof-toolbar-" (symbol-name token) "-enable-p")))
 
 ;;
 ;; Menu built from toolbar functions
 ;;
 
+(defun proof-toolbar-make-menu-item (tle)
+  "Make a menu item from a proof-toolbar-entries entry."
+  (let
+      ((token	  (car tle))
+       (menuname  (cadr tle))
+       (tooltip   (nth 2 tle))
+       (enablep	  (nth 3 tle)))
+    (apply 'vector
+	   (append
+	    (list menuname (proof-toolbar-function token))
+	    (if enablep 
+		(list ':active (list (proof-toolbar-enabler token))))))))
+   
 (defconst proof-toolbar-menu
-  ;; Toolbar contains commands to manipulate script: "Scripting"
-  '("Scripting"
-    ["Goal"
-     proof-toolbar-goal
-     :active (proof-toolbar-goal-enable-p)]
-    ["Retract"
-     proof-toolbar-retract
-     :active (proof-toolbar-retract-enable-p)]
-    ["Undo"
-     proof-toolbar-undo
-     :active (proof-toolbar-undo-enable-p)]
-    ["Next"
-     proof-toolbar-next
-     :active (proof-toolbar-next-enable-p)]
-    ["Use"
-     proof-toolbar-use
-     :active (proof-toolbar-use-enable-p)]
-    ["Restart"
-     proof-toolbar-restart
-     :active (proof-toolbar-restart-enable-p)]
-    ["QED"
-     proof-toolbar-qed
-     :active (proof-toolbar-qed-enable-p)])
-  "Menu made from the toolbar commands.")
+  ;; Toolbar contains commands to manipulate script and
+  ;; other handy stuff.  Called "Scripting"
+  (append
+   '("Scripting")
+   (mapcar 'proof-toolbar-make-menu-item 
+	   proof-toolbar-entries))
+  "Menu made from the Proof General toolbar commands.")
 
 ;;
 ;; Add this menu to proof-menu
@@ -69,21 +114,54 @@ prover specific buttons, see proof-toolbar.el.")
 (setq proof-menu
       (append proof-menu (list proof-toolbar-menu)))
 
+;;
+;; Now the toolbar icons and buttons
+;; 
+
+(defun proof-toolbar-make-icon (tle)
+  "Make icon variable and icon list entry from a proof-toolbar-entries entry."
+  (let* ((icon (car tle))
+	 (iconname (symbol-name icon))
+	 (iconvar  (proof-toolbar-icon icon)))
+    ;; first declare variable
+    ;;  (eval
+    ;;  `(defvar ,iconvar nil
+    ;;  ,(concat 
+    ;;   "Glyph list for " iconname " button in Proof General toolbar.")))
+    ;; FIXME: above doesn't quite work right.  However, we only lose
+    ;; the docstring which is no big deal.
+    ;; now the list entry
+    (list iconvar iconname)))
+  
 (defconst proof-toolbar-iconlist
-  '((proof-toolbar-next-icon "next")
-    (proof-toolbar-undo-icon "undo")
-    (proof-toolbar-retract-icon "retract")
-    (proof-toolbar-use-icon "use")
-    (proof-toolbar-goal-icon "goal")
-    (proof-toolbar-qed-icon  "qed")
-    (proof-toolbar-restart-icon "restart"))
+  (mapcar 'proof-toolbar-make-icon proof-toolbar-entries)
   "List of icon variable names and their associated image files.
 A list of lists of the form (VAR IMAGE).  IMAGE is the root name
 for an image file in proof-images-directory.  The toolbar
 code expects to find files IMAGE.xbm, IMAGE.xpm, IMAGE.8bit.xpm
 and chooses the best one for the display properites.")
 
-(defvar proof-toolbar-button-list proof-toolbar-default-button-list
+(defun proof-toolbar-make-toolbar-item (tle)
+  "Make a toolbar button descriptor from a proof-toolbar-entries entry."
+  (let
+      ((token	  (car tle))
+       (menuname  (cadr tle))
+       (tooltip   (nth 2 tle))
+       ;; FIXME: enabler now enabled, for testing at least.
+       ;; (enablep nil))
+       (enablep  (nth 3 tle)))
+    (vector
+     (proof-toolbar-icon token)
+     (proof-toolbar-function token)
+     (if enablep 
+	 (list (proof-toolbar-enabler token))
+       t)
+     tooltip)))
+
+(defvar proof-toolbar-button-list 
+  (append
+   (mapcar 'proof-toolbar-make-toolbar-item proof-toolbar-entries)
+   (list [:style 3d]))
   "A toolbar descriptor evaluated in proof-toolbar-setup.
 Specifically, a list of sexps which evaluate to entries in a toolbar
 descriptor.   The default value proof-toolbar-default-button-list
@@ -92,15 +170,6 @@ will work for any proof assistant.")
 (defvar proof-toolbar nil
   "Proof mode toolbar button list.  Set in proof-toolbar-setup.")
 
-;; FIXME: edit-toolbar cannot edit proof toolbar (even in a proof mode)
-;; Need a variable containing  a specifier or similar.
-;; (defvar proof-toolbar-specifier nil
-;;   "Specifier for proof toolbar.")
-;; This doesn't seem worth fixing until XEmacs toolbar implementation
-;; settles a bit.  Enablers don't work too well at the moment.
-
-;; FIXME: could automatically defvar the icon variables.
-
 ;;; ###autoload
 (defun proof-toolbar-setup ()
   "Initialize Proof General toolbar and enable it for the current buffer.
@@ -140,117 +209,30 @@ to the default toolbar."
        (or force-on (not proof-toolbar-inhibit)))
   (proof-toolbar-setup))
   
+
+;;
+;; =================================================================
 ;;
-;; GENERIC PROOF TOOLBAR BUTTONS
+;;
+;; GENERIC PROOF TOOLBAR BUTTON FUNCTIONS
 ;;
 ;; Defaults functions are provided below for: up, down, restart
 ;; Code for specific provers may define the symbols below to use
 ;; the other buttons: next, prev, goal, qed (images are provided).
 ;;
 ;;  proof-toolbar-next		   next function
-;;  proof-toolbar-next-enable    enable predicate for next (or t)
+;;  proof-toolbar-next-enable      enable predicate for next (or t)
 ;;
 ;; etc.
 ;;
 ;; To add support for more buttons or alter the default
-;; images, proof-toolbar-iconlist should be adjusted.
-;; 
+;; images, proof-toolbar-entries should be adjusted.
 ;;
-
-;; FIXME: In the future, add back the enabler functions.
-;; As of 20.4, they *almost* work, but it seems difficult
-;; to get the toolbar to update at the right times.
-;; For older versions of XEmacs (19.15, P.C.Callaghan@durham.ac.uk
-;; reports) the toolbar specifier format doesn't like
-;; arbitrary sexps as the enabler, either.
 ;;
 
-(defvar proof-toolbar-next-icon nil
-  "Glyph list for next button in proof toolbar.
-Initialised in proof-toolbar-setup.")
-
-(defvar proof-toolbar-next-button
-  [proof-toolbar-next-icon
-   proof-toolbar-next
-   ;; XEmacs isn't ready for enablers yet
-   t
-   ;; (proof-toolbar-next-enable-p)
-   "Process the next proof command"])
-
-(defvar proof-toolbar-undo-icon nil
-  "Glyph list for undo button in proof toolbar.
-Initialised in proof-toolbar-setup.")
-
-(defvar proof-toolbar-undo-button
-  [proof-toolbar-undo-icon
-   proof-toolbar-undo
-   ;; XEmacs isn't ready for enablers yet
-   t
-   ;; (proof-toolbar-undo-enable-p)
-   "Undo the previous proof command"])
-
-(defvar proof-toolbar-retract-icon nil
-  "Glyph list for retract button in proof toolbar.
-Initialised in proof-toolbar-setup.")
-
-(defvar proof-toolbar-retract-button
-  [proof-toolbar-retract-icon
-   proof-toolbar-retract
-   ;; XEmacs isn't ready for enablers yet
-   t
-   ;; (proof-toolbar-retract-enable-p)
-   "Retract buffer"])
-
-(defvar proof-toolbar-use-icon nil
-  "Glyph list for use button in proof toolbar.
-Initialised in proof-toolbar-setup.")
-
-(defvar proof-toolbar-use-button
-  [proof-toolbar-use-icon
-   proof-toolbar-use
-   ;; XEmacs isn't ready for enablers yet
-   t
-   ;; (proof-toolbar-use-enable-p)
-   "Process whole buffer"])
-
-(defvar proof-toolbar-restart-icon nil
-  "Glyph list for down button in proof toolbar.
-Initialised in proof-toolbar-setup.")
-
-(defvar proof-toolbar-restart-button
-  [proof-toolbar-restart-icon
-   proof-toolbar-restart
-   ;; XEmacs isn't ready for enablers yet
-   t
-   ;; (proof-toolbar-restart-enable-p)
-   "Restart scripting"])
-
-(defvar proof-toolbar-goal-icon nil
-    "Glyph list for goal button in proof toolbar.
-Initialised in proof-toolbar-setup.")
-
-(defvar proof-toolbar-goal-button
-  [proof-toolbar-goal-icon
-   proof-toolbar-goal
-   ;; XEmacs isn't ready for enablers yet
-   t
-   ;; (proof-toolbar-goal-enable-p)
-   "Start a new proof"])
-
-(defvar proof-toolbar-qed-icon nil
-    "Glyph list for QED button in proof toolbar.
-Initialised in proof-toolbar-setup.")
-
-(defvar proof-toolbar-qed-button
-  [proof-toolbar-qed-icon
-   proof-toolbar-qed
-   ;; XEmacs isn't ready for enablers yet
-   t
-   ;; (proof-toolbar-qed-enable-p)
-   "Save proved theorem"])
-
-;;
-;; GENERIC PROOF TOOLBAR FUNCTIONS
+
+;;
+;; Helper functions 
 ;;
 
 (defmacro proof-toolbar-move (&rest body)
@@ -267,7 +249,6 @@ Initialised in proof-toolbar-setup.")
     (proof-goto-end-of-queue-or-locked-if-not-visible)))
 
 
-
 ;;
 ;; Undo button
 ;;
@@ -391,8 +372,43 @@ Move point if the end of the locked position is invisible."
       (call-interactively 'proof-issue-save)
     (error "I can't see a completed proof!")))
 
+;;
+;; Show button
+;;
+
+(defun proof-toolbar-show-enable-p ()
+  (proof-shell-available-p))
+  
+(defalias 'proof-toolbar-show 'proof-prf)
 
+;;
+;; Context button
+;;
 
+(defun proof-toolbar-context-enable-p ()
+  (proof-shell-available-p))
+  
+(defalias 'proof-toolbar-context 'proof-ctxt)
+
+;;
+;; Info button
+;;
+;; Might as well enable it all the time; convenient
+;; way of starting proof assistant.
 
+(defun proof-toolbar-info-enable-p ()
+  t)
+
+(defalias 'proof-toolbar-info 'proof-help)
+
+;;
+;; Command button
+;;
+
+(defun proof-toolbar-command-enable-p ()
+  (proof-shell-available-p))
+
+(defalias 'proof-toolbar-command 'proof-execute-minibuffer-cmd)
+  
 ;; 
 (provide 'proof-toolbar)