save settings not defined with defpacustom (fixes #142)

- infrastructure for saving/resetting customizations not defined
  with defpacustom
- improve Coq -> Auto Compilation menu
- polish documentation and manual

3 files changed, 26 insertions, 4 deletions

diff --git a/generic/pg-pamacs.el b/generic/pg-pamacs.el
index bb765c2c..4958b360 100644
--- a/generic/pg-pamacs.el
+++ b/generic/pg-pamacs.el
@@ -228,7 +228,9 @@ which can be changed by sending commands.
 In this case, NAME stands for the internal setting, flag, etc,
 for the proof assistant, and a :setting and :type value should be
 provided.  The :type of NAME should be one of 'integer, 'float,
-'boolean, 'string.
+'boolean, 'string. Other types are not supported (see
+`proof-menu-entry-for-setting'). They will yield an error when
+constructing the proof assistant menu.
 
 The function `proof-assistant-format' is used to format VAL.
 
diff --git a/generic/pg-vars.el b/generic/pg-vars.el
index 3aafa97d..8d93a60b 100644
--- a/generic/pg-vars.el
+++ b/generic/pg-vars.el
@@ -209,7 +209,25 @@ and the function `proof-assistant-format'.  The TYPE item determines
 the form of the menu entry for the setting (this is an Emacs widget type)
 and the DESCR description string is used as a help tooltip in the settings menu.
 
-This list is extended by the `defpacustom' macro.")
+As TYPE's only the simple types boolean, integer, number and
+string are supported (see `proof-menu-entry-for-setting'). Other
+types will yield an error when constructing the proof assistant
+menu from this list.
+
+Customizations defined with `defpacustom' are automatically added
+to this list.")
+
+(defvar proof-assistant-additional-settings nil
+  "Additional proof assistant specific customizations (as list of symbols).
+This variable should hold those proof assistant specific
+customizations that are not included in
+`proof-assistant-settings' but which should be saved/restored
+with the save and reset settings menu entry in the proof
+assistant menu.
+
+Customization variables are missing in `proof-assistant-settings'
+when they have a type not supported by `defpacusom'.")
+
 
 (defvar pg-tracing-slow-mode nil
   "Non-nil for slow refresh mode for tracing output.")
diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index d4e0f803..df617347 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -921,8 +921,10 @@ KEY is the optional key binding."
 
 (defun proof-settings-vars ()
   "Return a list of proof assistant setting variables."
-  (mapcar (lambda (setting) (proof-ass-symv (car setting)))
-	  proof-assistant-settings))
+  (append
+   (mapcar (lambda (setting) (proof-ass-symv (car setting)))
+	   proof-assistant-settings)
+   proof-assistant-additional-settings))
 
 (defun proof-settings-changed-from-defaults-p ()
   ;; FIXME: would be nice to add.  Custom support?