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

1 files changed, 62 insertions, 28 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