Make <PA>-toolbar-entries, and move it and proof-toolbar-entries-default to proof-config to allow easier configuration.

2 files changed, 56 insertions, 13 deletions

diff --git a/generic/proof-config.el b/generic/proof-config.el
index 44adbddb..ffb79504 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -20,7 +20,7 @@
 ;;
 ;;     CONFIGURATION VARIABLES
 ;;  2. Major modes
-;;  3. Menus, user-level commands.
+;;  3. Menus, user-level commands, toolbar
 ;;  4. Script mode configuration 
 ;;  5. Shell mode configuration
 ;;     5a. commands
@@ -639,7 +639,7 @@ command line options.  For an example, see coq/coq.el."
 
 
 ;;
-;; 3. Configuration for menus, user-level commands, etc.
+;; 3. Configuration for menus, user-level commands, toolbar, etc.
 ;;
 
 (defcustom proof-assistant-home-page ""
@@ -724,6 +724,45 @@ conversion, etc.  (No changes are done if nil)."
   :type '(choice string nil)
   :group 'prover-config)
 
+(defconst proof-toolbar-entries-default
+  `((state	"Display proof state" "Display the current proof state" t)
+    (context	"Display context"     "Display the current context" t)
+    (goal	"Start a new proof"   "Start a new proof" t)
+    (retract	"Retract buffer"      "Retract (undo) whole buffer" t)
+    (undo	"Undo step"           "Undo the previous proof command" t)
+    (delete	"Delete step"         nil t)
+    (next	"Next step"           "Process the next proof command" t)
+    (use	"Use buffer"  	      "Process whole buffer" t)
+    (goto	"Goto point"	      "Process or undo to the cursor position" t)
+    (restart	"Restart scripting"   "Restart scripting (clear all locked regions)" t)
+    (qed	"Finish proof"        "Close/save proved theorem" t)
+    (lockedend  "Locked end"	      nil t)
+    (find	"Find theorems"	      "Find theorems" t)
+    (command    "Issue command"	      "Issue a non-scripting command" t)
+    (interrupt  "Interrupt prover"    "Interrupt the proof assistant (warning: may break synchronization)" t)
+    (info	nil		      "Show online proof assistant information" t)
+    (help	nil		      "Proof General manual" t))
+"Example value for proof-toolbar-entries.  Also used to define Scripting menu.
+This gives a bare toolbar that works for any prover, providing the
+appropriate configuration variables are set.
+To add/remove prover specific buttons, adjust the `<PA>-toolbar-entries' 
+variable, and follow the pattern in `proof-toolbar.el' for 
+defining functions, images.")
+
+
+(defpgcustom toolbar-entries proof-toolbar-entries-default
+  "List of entries for Proof General toolbar and Scripting menu.
+Format of each entry is (TOKEN MENUNAME TOOLTIP 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.
+If MENUNAME is nil, item will not appear on the scripting menu.
+If TOOLTIP is nil, item will not appear on the toolbar.
+
+The default value is `proof-toolbar-entries-default' which contains
+the standard Proof General buttons.")
+
+
 
 
 ;;
diff --git a/generic/proof-toolbar.el b/generic/proof-toolbar.el
index b9cefe13..67eddaa0 100644
--- a/generic/proof-toolbar.el
+++ b/generic/proof-toolbar.el
@@ -65,16 +65,18 @@ This gives a bare toolbar that works for any prover.  To add
 prover specific buttons, see documentation for proof-toolbar-entries
 and the file proof-toolbar.el.")
 
-;; FIXME: defcustom next one, to set on a per-prover basis
-(defvar proof-toolbar-entries
-  proof-toolbar-entries-default
+
+(defpgcustom toolbar-entries proof-toolbar-entries-default
   "List of entries for Proof General toolbar and Scripting menu.
 Format of each entry is (TOKEN MENUNAME TOOLTIP 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.
 If MENUNAME is nil, item will not appear on the scripting menu.
-If TOOLTIP is nil, item will not appear on the toolbar.")
+If TOOLTIP is nil, item will not appear on the toolbar.
+
+The default value is `proof-toolbar-entries-default' which contains
+the standard Proof General buttons.")
 
 
 
@@ -97,7 +99,7 @@ If TOOLTIP is nil, item will not appear on the toolbar.")
 ;; 
 
 (defun proof-toolbar-make-icon (tle)
-  "Make icon variable and icon list entry from a proof-toolbar-entries entry."
+  "Make icon variable and icon list entry from a PA-toolbar-entries entry."
   (let* ((icon (car tle))
 	 (iconname (symbol-name icon))
 	 (iconvar  (proof-toolbar-icon icon)))
@@ -112,7 +114,8 @@ If TOOLTIP is nil, item will not appear on the toolbar.")
     (list iconvar iconname)))
   
 (defconst proof-toolbar-iconlist
-  (mapcar 'proof-toolbar-make-icon proof-toolbar-entries)
+  (mapcar 'proof-toolbar-make-icon 
+	  (proof-ass 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
@@ -120,7 +123,7 @@ code expects to find files IMAGE.xbm, IMAGE.xpm, IMAGE.8bit.xpm
 and chooses the best one for the display properites.")
 
 (defun proof-toolbar-make-toolbar-item (tle)
-  "Make a toolbar button descriptor from a proof-toolbar-entries entry."
+  "Make a toolbar button descriptor from a PA-toolbar-entries entry."
   (let*
       ((token	      (car tle))
        (menuname      (cadr tle))
@@ -144,7 +147,8 @@ and chooses the best one for the display properites.")
 
 (defvar proof-toolbar-button-list 
   (append
-   (apply 'append (mapcar 'proof-toolbar-make-toolbar-item proof-toolbar-entries))
+   (apply 'append (mapcar 'proof-toolbar-make-toolbar-item 
+			  (proof-ass 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
@@ -266,7 +270,7 @@ changed state."
 ;; etc.
 ;;
 ;; To add support for more buttons or alter the default
-;; images, proof-toolbar-entries should be adjusted.
+;; images, <PA>-toolbar-entries should be adjusted.
 ;;
 ;;
 
@@ -461,7 +465,7 @@ changed state."
 ;;
 
 (defun proof-toolbar-make-menu-item (tle)
-  "Make a menu item from a proof-toolbar-entries entry."
+  "Make a menu item from a PA-toolbar-entries entry."
   (let*
       ((token	  (car tle))
        (menuname  (cadr tle))
@@ -487,7 +491,7 @@ changed state."
   ;; other handy stuff.  
   (apply 'append
 	  (mapcar 'proof-toolbar-make-menu-item 
-		  proof-toolbar-entries))
+		  (proof-ass toolbar-entries)))
   "Menu made from the Proof General toolbar commands.")