diff options
author | Hendrik Tews <hendrik@askra.de> | 2017-01-19 11:40:28 +0100 |
---|---|---|
committer | Hendrik Tews <hendrik@askra.de> | 2017-01-19 11:40:28 +0100 |
commit | 4bcac92df46da9e68b5e3d565bb118fb63b4feb4 (patch) | |
tree | ec19916cf72884ee83fc7f52d8c7d87b83ce767f /coq/coq-compile-common.el | |
parent | 77c3f2eac868f177b73d2aa59b277e40fc48fd0c (diff) |
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
Diffstat (limited to 'coq/coq-compile-common.el')
-rw-r--r-- | coq/coq-compile-common.el | 21 |
1 files changed, 17 insertions, 4 deletions
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) |