From 4bcac92df46da9e68b5e3d565bb118fb63b4feb4 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Thu, 19 Jan 2017 11:40:28 +0100 Subject: 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 --- coq/coq-abbrev.el | 90 ++++++++++++++++++++++++++++++++--------------- coq/coq-compile-common.el | 21 ++++++++--- coq/coq.el | 6 ++++ doc/PG-adapting.texi | 4 +-- doc/ProofGeneral.texi | 14 ++++++-- generic/pg-pamacs.el | 4 ++- generic/pg-vars.el | 20 ++++++++++- generic/proof-menu.el | 6 ++-- 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? -- cgit v1.2.3