From e9ac9e8eb3d2567ff1ab12cf7bfdd60d5df2c30f Mon Sep 17 00:00:00 2001
From: David Aspinall <da@inf.ed.ac.uk>
Date: Mon, 1 May 2000 18:18:30 +0000
Subject: Added proof-assistant-menu-entries for proof assistant specific
 menus.

---
 generic/proof-config.el |  7 +++++++
 generic/proof-script.el | 17 +++++++++++++++--
 2 files changed, 22 insertions(+), 2 deletions(-)

(limited to 'generic')

diff --git a/generic/proof-config.el b/generic/proof-config.el
index 874a53fc..dc39cc62 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -682,6 +682,13 @@ If a function, it should return the command string to insert."
   :type '(choice string function)
   :group 'prover-config)
 
+(defcustom proof-assistant-menu-entries nil
+  "Entries for proof assistant specific menu. 
+A list of menu items [NAME CALLBACK ENABLE].  See the documentation
+of `easy-menu-define' for more details."
+  :type 'sexp
+  :group 'prover-config)
+
 
 
 
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 6d2708b2..933bf1df 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -2346,8 +2346,11 @@ This is intended as a value for proof-activate-scripting-hook"
 	     :active (fboundp 'function-menu)]
 	    "----")
           proof-shared-menu)
-  "The menu for the proof assistant.")
+  "The Proof General generic menu.")
 
+(defvar proof-assistant-menu
+  nil
+  "The Proof General proof-assistant specific menu.")
 
 
 
@@ -2723,7 +2726,7 @@ finish setup which depends on specific proof assistant configuration."
   ;; NB: autloads proof-toolbar, which defines proof-toolbar-scripting-menu.
   (proof-toolbar-setup)
 
-  ;; Menu
+  ;; Menus
   (easy-menu-define proof-mode-menu  
 		    proof-mode-map
 		    "Proof General menu"
@@ -2748,6 +2751,16 @@ finish setup which depends on specific proof assistant configuration."
   ;; Put the ProofGeneral menu on the menubar
   (easy-menu-add proof-mode-menu proof-mode-map)
 
+  ;; Deal with the proof assistant specific menu 
+  (if proof-assistant-menu-entries
+      (progn
+	(easy-menu-define proof-assistant-menu 
+			  proof-mode-map
+			  proof-assistant
+			  (cons proof-assistant
+				proof-assistant-menu-entries))
+	(easy-menu-add proof-assistant-menu proof-mode-map)))
+
 
   ;; Make sure func menu is configured.  (NB: Ideal place for this and
   ;; similar stuff would be in something evaluated at top level after
-- 
cgit v1.2.3