From dae4fc095488a023cfacecb089eb6ff7d004a7c5 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Tue, 28 Sep 1999 14:44:15 +0000
Subject: Made Scripting menu entry item on menubar.

---
 generic/proof-script.el | 15 ++++++++++++---
 1 file changed, 12 insertions(+), 3 deletions(-)

(limited to 'generic/proof-script.el')

diff --git a/generic/proof-script.el b/generic/proof-script.el
index 72fafb34..a2858768 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -1821,14 +1821,18 @@ finish setup which depends on specific proof assistant configuration."
   (if proof-script-indent
       (setq indent-line-function 'proof-indent-line))
 
-  ;; Toolbar
-  ;; (NB: autloads proof-toolbar, which extends proof-menu variable)
+  ;; 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  
 		    proof-mode-map
-		    "Menu used in Proof General scripting mode."
+		    "Proof General menu"
 		    (cons proof-general-name
 			  (append
 			   (cdr proof-menu)
@@ -1843,7 +1847,12 @@ finish setup which depends on specific proof assistant configuration."
 			     nil)
 			   ;; end UGLY COMPATIBILTY HACK
 			   )))
+
+  ;; Put the ProofGeneral menu first on the menubar, then Scripting menu
+  ;; (makes Scripting menu more obvious)
   (easy-menu-add proof-mode-menu proof-mode-map)
+  (easy-menu-add proof-mode-script-menu proof-mode-map)
+
 
   ;; For fontlock
 
-- 
cgit v1.2.3