Reorganization of menus: made a single menu but flattened Scripting submenu.

3 files changed, 73 insertions, 62 deletions

diff --git a/generic/proof-script.el b/generic/proof-script.el
index a2858768..c8baac64 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -1585,25 +1585,26 @@ No action if BUF is nil."
 (defvar proof-shared-menu
   (append
     (list
-     ["Display proof state"
-      proof-prf
-      :active (proof-shell-live-buffer)]
-     ["Display context"
-      proof-ctxt
-      :active (proof-shell-live-buffer)]
-     ["Find theorems"
-      proof-find-theorems
-      :active (proof-shell-live-buffer)]
+;     ["Display proof state"
+;      proof-prf
+;      :active (proof-shell-live-buffer)]
+;     ["Display context"
+;      proof-ctxt
+;      :active (proof-shell-live-buffer)]
+;     ["Find theorems"
+;      proof-find-theorems
+;      :active (proof-shell-live-buffer)]
      ["Start proof assistant"
       proof-shell-start
       :active (not (proof-shell-live-buffer))]
-     ["Restart scripting"
-      proof-shell-restart
-      :active (proof-shell-live-buffer)]
+;     ["Restart scripting"
+;      proof-shell-restart
+;      :active (proof-shell-live-buffer)]
      ["Exit proof assistant"
       proof-shell-exit
       :active (proof-shell-live-buffer)])
     (list proof-help-menu)
+    (list proof-buffer-menu)
     ;; Would be nicer to put this at the bottom, but it's
     ;; a bit tricky then to get it in all menus.
     ;; UGLY COMPATIBILITY  FIXME: remove this soon
@@ -1616,12 +1617,11 @@ No action if BUF is nil."
     ;; UGLY COMPATIBILITY  FIXME: remove this soon
     (list (if (string-match "XEmacs 19.1[2-9]" emacs-version)
 	      "--:doubleLine" "----"))
-    (list proof-buffer-menu))
+    )
   "Proof General menu for various modes.")
 
 (defvar proof-menu  
-  (append '("Commands"
-            ["Active terminator" proof-active-terminator-minor-mode
+  (append '(["Active terminator" proof-active-terminator-minor-mode
 	     :active t
 	     :style toggle
              :selected proof-active-terminator-minor-mode]
@@ -1824,10 +1824,6 @@ finish setup which depends on specific proof assistant configuration."
   ;; Toolbar and scripting menu
   ;; NB: autloads proof-toolbar, which defines proof-toolbar-scripting-menu.
   (proof-toolbar-setup)
-  (easy-menu-define proof-mode-script-menu
-		    proof-mode-map
-		    "Scripting menu of Proof General"
-		    proof-toolbar-scripting-menu)
 
   ;; Menu
   (easy-menu-define proof-mode-menu  
@@ -1835,7 +1831,8 @@ finish setup which depends on specific proof assistant configuration."
 		    "Proof General menu"
 		    (cons proof-general-name
 			  (append
-			   (cdr proof-menu)
+			   proof-toolbar-scripting-menu
+			   proof-menu
 			   ;; begin UGLY COMPATIBILTY HACK
 			   ;; older/non-existent customize doesn't have 
 			   ;; this function.  
@@ -1848,11 +1845,8 @@ finish setup which depends on specific proof assistant configuration."
 			   ;; end UGLY COMPATIBILTY HACK
 			   )))
 
-  ;; Put the ProofGeneral menu first on the menubar, then Scripting menu
-  ;; (makes Scripting menu more obvious)
+  ;; Put the ProofGeneral menu on the menubar
   (easy-menu-add proof-mode-menu proof-mode-map)
-  (easy-menu-add proof-mode-script-menu proof-mode-map)
-
 
   ;; For fontlock
 
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 24ae9e5e..6e9f7f0a 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1514,7 +1514,7 @@ before and after sending the command."
 (easy-menu-define proof-shell-mode-menu
 		  proof-shell-mode-map
 		  "Menu used in Proof General shell mode."
-		  (cons proof-general-name (cdr proof-shell-menu)))
+		  (cons proof-general-name proof-shell-menu))
 
 
 
diff --git a/generic/proof-toolbar.el b/generic/proof-toolbar.el
index 445b7382..bea72456 100644
--- a/generic/proof-toolbar.el
+++ b/generic/proof-toolbar.el
@@ -41,8 +41,9 @@
 
 
 ;;
-;; The default generic toolbar
+;; The default generic toolbar and toolbar variable
 ;;
+
 (defconst proof-toolbar-entries-default
   `((state	"Display proof state" "Display the current proof state" t)
     (context	"Display context"     "Display the current context" t)
@@ -57,14 +58,15 @@
     (command    "Issue command"	      "Issue a non-scripting command" t)
     (info	nil		      "Show proof assistant information" t)
     (help	nil		      "Proof General manual" t))
-"Example value for proof-toolbar-entries.
+"Example value for proof-toolbar-entries.  Also used to define Scripting menu.
 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
-  "List of entries for Proof General toolbar.
+  "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>,
@@ -72,6 +74,7 @@ For each TOKEN, we expect an icon with base filename TOKEN,
 If MENUNAME is nil, item will not appear on the \"Scripting\" menu.")
 
 
+
 ;;
 ;; Function, icon, button names
 ;; 
@@ -85,40 +88,6 @@ If MENUNAME is nil, item will not appear on the \"Scripting\" menu.")
 (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)))
-    (if menuname
-	(list 
-	 (apply 'vector
-	   (append
-	    (list menuname (proof-toolbar-function token))
-	    (if enablep 
-		(list ':active (list (proof-toolbar-enabler token))))))))))
-   
-(defconst proof-toolbar-scripting-menu
-  ;; Toolbar contains commands to manipulate script and
-  ;; other handy stuff.  Called "Scripting"
-  (append
-   '("Scripting")
-   (apply 'append
-	  (mapcar 'proof-toolbar-make-menu-item 
-		  proof-toolbar-entries)))
-  "Menu made from the Proof General toolbar commands.")
-
-;;
-;; Add this menu to proof-menu
-;;
-; (setq proof-menu
-;      (append proof-menu (list proof-toolbar-menu)))
 
 ;;
 ;; Now the toolbar icons and buttons
@@ -173,6 +142,10 @@ Specifically, a list of sexps which evaluate to entries in a toolbar
 descriptor.   The default value proof-toolbar-default-button-list
 will work for any proof assistant.")
 
+;;
+;; Code for displaying and refreshing toolbar
+;;
+
 (defvar proof-toolbar nil
   "Proof mode toolbar button list.  Set in proof-toolbar-setup.")
 
@@ -460,6 +433,50 @@ Move point if the end of the locked position is invisible."
 
 (defalias 'proof-toolbar-find 'proof-find-theorems)
 
+
+;;
+;; =================================================================
+;;
+;; Scripting 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))
+       (fnname	  (proof-toolbar-function token))
+       ;; fnval: remove defalias to get keybinding onto menu; 
+       ;; NB: function and alias must both be defined for this 
+       ;; to work!!
+       (fnval	  (if (symbolp (symbol-function fnname))
+		      (symbol-function fnname)
+		    fnname)))
+    (if menuname
+	(list 
+	 (apply 'vector
+	   (append
+	    (list menuname fnval)
+	    (if enablep 
+		(list ':active (list (proof-toolbar-enabler token))))))))))
+   
+(defconst proof-toolbar-scripting-menu
+  ;; Toolbar contains commands to manipulate script and
+  ;; other handy stuff.  Called "Scripting"
+  (apply 'append
+	  (mapcar 'proof-toolbar-make-menu-item 
+		  proof-toolbar-entries))
+  "Menu made from the Proof General toolbar commands.")
+
+;;
+;; Add this menu to proof-menu
+;;
+; (setq proof-menu
+;      (append proof-menu (list proof-toolbar-menu)))
+
  
 ;; 
 (provide 'proof-toolbar)
+