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

8 files changed, 124 insertions, 41 deletions

diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index 534c013d..2b318dea 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -169,34 +169,68 @@ It was constructed with `proof-defstringset-fn'.")
 		   coq-compile-parallel-in-background)
       :help ,(concat "Continue background compilation after "
 		     "the first error as far as possible")]
-    ["no quick"
-      (customize-set-variable 'coq-compile-quick 'no-quick)
-      :style radio
-      :selected (eq coq-compile-quick 'no-quick)
-      :active (and coq-compile-before-require
-		   coq-compile-parallel-in-background)
-      :help "Compile without -quick but accept existion .vio's"]
-     ["quick no vio2vo"
-      (customize-set-variable 'coq-compile-quick 'quick-no-vio2vo)
-      :style radio
-      :selected (eq coq-compile-quick 'quick-no-vio2vo)
-      :active (and coq-compile-before-require
-		   coq-compile-parallel-in-background)
-      :help "Compile with -quick, accept existing .vo's, don't run vio2vo"]
-     ["quick and vio2vo"
-      (customize-set-variable 'coq-compile-quick 'quick-and-vio2vo)
-      :style radio
-      :selected (eq coq-compile-quick 'quick-and-vio2vo)
-      :active (and coq-compile-before-require
-		   coq-compile-parallel-in-background)
-      :help "Compile with -quick, accept existing .vo's, run vio2vo later"]
-     ["ensure vo"
-      (customize-set-variable 'coq-compile-quick 'ensure-vo)
-      :style radio
-      :selected (eq coq-compile-quick 'ensure-vo)
-      :active (and coq-compile-before-require
-		   coq-compile-parallel-in-background)
-      :help "Ensure only vo's are used for consistency"]
+     ("Quick compilation"
+      ["no quick"
+       (customize-set-variable 'coq-compile-quick 'no-quick)
+       :style radio
+       :selected (eq coq-compile-quick 'no-quick)
+       :active (and coq-compile-before-require
+		    coq-compile-parallel-in-background)
+       :help "Compile without -quick but accept existion .vio's"]
+      ["quick no vio2vo"
+       (customize-set-variable 'coq-compile-quick 'quick-no-vio2vo)
+       :style radio
+       :selected (eq coq-compile-quick 'quick-no-vio2vo)
+       :active (and coq-compile-before-require
+		    coq-compile-parallel-in-background)
+       :help "Compile with -quick, accept existing .vo's, don't run vio2vo"]
+      ["quick and vio2vo"
+       (customize-set-variable 'coq-compile-quick 'quick-and-vio2vo)
+       :style radio
+       :selected (eq coq-compile-quick 'quick-and-vio2vo)
+       :active (and coq-compile-before-require
+		    coq-compile-parallel-in-background)
+       :help "Compile with -quick, accept existing .vo's, run vio2vo later"]
+      ["ensure vo"
+       (customize-set-variable 'coq-compile-quick 'ensure-vo)
+       :style radio
+       :selected (eq coq-compile-quick 'ensure-vo)
+       :active (and coq-compile-before-require
+		    coq-compile-parallel-in-background)
+       :help "Ensure only vo's are used for consistency"]
+      )
+     ("Auto Save"
+      ["Query coq buffers"
+       (customize-set-variable 'coq-compile-auto-save 'ask-coq)
+       :style radio
+       :selected (eq coq-compile-auto-save 'ask-coq)
+       :active coq-compile-before-require
+       :help "Ask for each coq-mode buffer, except the current buffer"]
+      ["Query all buffers"
+       (customize-set-variable 'coq-compile-auto-save 'ask-all)
+       :style radio
+       :selected (eq coq-compile-auto-save 'ask-all)
+       :active coq-compile-before-require
+       :help "Ask for all buffers"]
+      ["Autosave coq buffers"
+       (customize-set-variable 'coq-compile-auto-save 'save-coq)
+       :style radio
+       :selected (eq coq-compile-auto-save 'save-coq)
+       :active coq-compile-before-require
+       :help "Save all Coq buffers without confirmation, except the current one"]
+      ["Autosave all buffers"
+       (customize-set-variable 'coq-compile-auto-save 'save-all)
+       :style radio
+       :selected (eq coq-compile-auto-save 'save-all)
+       :active coq-compile-before-require
+       :help "Save all buffers without confirmation"]
+      )
+     ["Lock Ancesotors"
+      coq-lock-ancestors-toggle
+      :style toggle
+      :selected coq-lock-ancestors
+      :active coq-compile-before-require
+      :help "Lock files of imported modules"]
      ["Confirm External Compilation"
       coq-confirm-external-compilation-toggle
       :style toggle
diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el
index 4b0033d1..72a16881 100644
--- a/coq/coq-compile-common.el
+++ b/coq/coq-compile-common.el
@@ -246,7 +246,10 @@ quick-and-vio2vo Same as `quick-no-vio2vo', but start vio2vo processes
 ensure-vo        Ensure that all library dependencies are present as .vo
                  files and delete outdated .vio files or .vio files that
                  are more recent than the corresponding .vo file. This
-                 setting is the only one that ensures soundness."
+                 setting is the only one that ensures soundness.
+
+This option can be set via menu
+`Coq -> Auto Compilation -> Quick compilation'."
   :type
   '(radio
     (const :tag "don't use -quick but accept existing vio files" no-quick)
@@ -371,7 +374,10 @@ This makes four permitted values: 'ask-coq to confirm saving all
 modified Coq buffers, 'ask-all to confirm saving all modified
 buffers, 'save-coq to save all modified Coq buffers without
 confirmation and 'save-all to save all modified buffers without
-confirmation."
+confirmation.
+
+This option can be set via menu
+`Coq -> Auto Compilation -> Auto Save'."
   :type
   '(radio
     (const :tag "ask for each coq-mode buffer, except the current buffer"
@@ -389,17 +395,24 @@ confirmation."
   "If non-nil, lock ancestor module files.
 If external compilation is used (via `coq-compile-command') then
 only the direct ancestors are locked. Otherwise all ancestors are
-locked when the \"Require\" command is processed."
+locked when the \"Require\" command is processed.
+
+This option can be set via menu
+`Coq -> Auto Compilation -> Lock Ancestors'."
+
   :type 'boolean
   :safe 'booleanp
   :group 'coq-auto-compile)
 
+;; define coq-lock-ancestors-toggle
+(proof-deftoggle coq-lock-ancestors)
+
 (defpacustom confirm-external-compilation t
   "If set let user change and confirm the compilation command.
 Otherwise start the external compilation without confirmation.
 
 This option can be set/reset via menu
-`Coq -> Settings -> Confirm External Compilation'."
+`Coq -> Auto Compilation -> Confirm External Compilation'."
   :type 'boolean
   :group 'coq-auto-compile)
 
diff --git a/coq/coq.el b/coq/coq.el
index edf905ae..f6c67475 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1544,6 +1544,12 @@ Near here means PT is either inside or just aside of a comment."
 ;; FIXME da: Does Coq have a help or about command?
 ;;	proof-info-command "Help"
 
+  ;; Settings not defined with defpacustom because they have an unsupported
+  ;; type.
+  (setq proof-assistant-additional-settings
+        '(coq-compile-quick coq-compile-keep-going
+          coq-compile-auto-save coq-lock-ancestors))
+
   (setq proof-goal-command-p 'coq-goal-command-p
         proof-find-and-forget-fn 'coq-find-and-forget
         pg-topterm-goalhyplit-fn 'coq-goal-hyp
diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi
index cf88d683..44c40549 100644
--- a/doc/PG-adapting.texi
+++ b/doc/PG-adapting.texi
@@ -361,7 +361,7 @@ file for the mode, which will be
 where @var{proof-home-directory} is the value of the
 variable @samp{@code{proof-home-directory}}.
 
-The default value is @code{((isar "Isabelle" "thy") (coq "Coq" "v" nil (".vo" ".glob")) (phox "PhoX" "phx") (pgshell "PG-Shell" "pgsh") (pgocaml "PG-OCaml" "pgml") (pghaskell "PG-Haskell" "pghci"))}.
+The default value is @code{((isar "Isabelle" "thy") (coq "Coq" "v" nil (".vo" ".glob")) (easycrypt "EasyCrypt" "ec" ".*\\.eca?") (pgshell "PG-Shell" "pgsh") (pgocaml "PG-OCaml" "pgml") (pghaskell "PG-Haskell" "pghci"))}.
 @end defopt
 
 
@@ -3258,7 +3258,7 @@ in the @code{proof-assistants} setting.
 @c TEXI DOCSTRING MAGIC: proof-assistants
 @defopt proof-assistants 
 Choice of proof assistants to use with Proof General.@*
-A list of symbols chosen from: @code{'isar} @code{'coq} @code{'phox} @code{'pgshell} @code{'pgocaml} @code{'pghaskell}.
+A list of symbols chosen from: @code{'isar} @code{'coq} @code{'easycrypt} @code{'pgshell} @code{'pgocaml} @code{'pghaskell}.
 If nil, the default will be ALL available proof assistants.
 
 Each proof assistant defines its own instance of Proof General,
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 442ce6d5..8dab17f0 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -4667,8 +4667,9 @@ ancestor.
 You have two choices, if you don't like ancestor locking in its
 default way.
 You can either switch ancestor locking completely off via
+menu @code{Coq -> Auto Compilation -> Lock Ancestors} or
 @code{coq-lock-ancestors} (@ref{Customizing Coq Multiple
-File Support}) or you can generally permit editing in locked
+File Support}). Alternatively, you can generally permit editing in locked
 sections with selecting 
 @code{Proof-General} -> @code{Quick Options} -> @code{Read Only}
 -> @code{Freely Edit} (which will set the option
@@ -4689,7 +4690,8 @@ file.]
 Proof General supports quick compilation only with the parallel
 asynchronous compilation. There are 4 modes that can be
 configured with @code{coq-compile-quick} or by selecting one of
-the radio buttons in the @code{Coq -> Auto Compilation} menu.
+the radio buttons in the @code{Coq -> Auto Compilation -> Quick
+compilation} menu.
 
 Use the default @code{no-quick}, if you have not yet switched to
 @code{Proof using}. Use @code{quick-no-vio2vo}, if you want quick
@@ -4824,6 +4826,9 @@ modified Coq buffers, @code{'ask-all} to confirm saving all modified
 buffers, @code{'save-coq} to save all modified Coq buffers without
 confirmation and @code{'save-all} to save all modified buffers without
 confirmation.
+
+This option can be set via menu
+@samp{Coq -> Auto Compilation -> Auto Save}.
 @end defvar
 
 
@@ -4899,6 +4904,9 @@ If non-nil, lock ancestor module files.@*
 If external compilation is used (via @samp{@code{coq-compile-command}}) then
 only the direct ancestors are locked. Otherwise all ancestors are
 locked when the "Require" command is processed.
+
+This option can be set via menu
+@samp{Coq -> Auto Compilation -> Lock Ancestors}.
 @end defvar
 
 
@@ -4942,7 +4950,7 @@ If set let user change and confirm the compilation command.@*
 Otherwise start the external compilation without confirmation.
 
 This option can be set/reset via menu
-@samp{Coq -> Settings -> Confirm External Compilation}.
+@samp{Coq -> Auto Compilation -> Confirm External Compilation}.
 @end defvar
 
 
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?