Fixup menus.

2 files changed, 17 insertions, 14 deletions

diff --git a/generic/proof-config.el b/generic/proof-config.el
index 30c1c2e0..05006440 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -1896,21 +1896,23 @@ X-Symbol support is deactivated."
 ;; NB: this section is work in progress
 
 (defmacro proof-defasscustom (sym &rest args)
-  `(defcustom ,(intern (concat (symbol-name
-				proof-assistant-symbol)
+  `(defcustom ,(intern (concat (symbol-name proof-assistant-symbol)
+			       "-"
 			       (symbol-name sym)))
-     :group ,(quote proof-assistant-cusgrp)
-     ,@args))
+     ,@args
+     ;; Would be nicer to put group earlier so it might be
+     ;; overriden in real call, but that means taking apart args.
+     :group ,(quote proof-assistant-cusgrp)))
 
-; (proof-defasscustom favourites nil
-;  "
-		    
+(defmacro proof-ass (sym)
+  "Return the value of SYM for the current prover."
+  (intern (concat (symbol-name proof-assistant-symbol)
+		  "-"
+		  (symbol-name sym))))
 
-		    
 
-;(proof-defass-custom test "Hello"
-;  "Command"
-;  :type 'string)
+(proof-defasscustom favourites nil
+  "Favourites on proof assistant specific menu.")
 		     
 
 
diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index a2a390a9..28969717 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -74,8 +74,9 @@
 	  proof-menu
 	  (list "----")
 	  (append
-	   (customize-menu-create 'proof-general)
-	   (customize-menu-create 'proof-general-internals "Internals"))
+	   (list (customize-menu-create 'proof-general))
+	   (list (customize-menu-create 'proof-general-internals 
+					"Internals")))
 	  proof-bug-report-menu))))
 
 
@@ -90,7 +91,7 @@
    (cons proof-assistant
 	 (append
 	  proof-assistant-menu-entries
-	  proof-assistant-favourites
+	  (proof-ass favourites)
 	  '("----")
 	  '(["Add favourite" 
 	     (call-interactively 'proof-add-favourite) t])))))