diff options
Diffstat (limited to 'coq/coq-abbrev.el')
| -rw-r--r-- | coq/coq-abbrev.el | 61 |
1 files changed, 61 insertions, 0 deletions
diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index 9432bd1b..534c013d 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -148,6 +148,67 @@ It was constructed with `proof-defstringset-fn'.") :style toggle :selected coq-double-hit-enable :help "Automatically send commands when terminator typed twiced quickly."] + ("Auto Compilation" + ["Compile Before Require" + coq-compile-before-require-toggle + :style toggle + :selected coq-compile-before-require + :help "Check dependencies of required modules and compile on the fly."] + ["Parallel background compilation" + coq-compile-parallel-in-background-toggle + :style toggle + :selected coq-compile-parallel-in-background + :active coq-compile-before-require + :help ,(concat "Compile parallel in background or " + "sequentially with blocking ProofGeneral.")] + ["Keep going" + coq-compile-keep-going-toggle + :style toggle + :selected coq-compile-keep-going + :active (and coq-compile-before-require + 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"] + ["Confirm External Compilation" + coq-confirm-external-compilation-toggle + :style toggle + :selected coq-confirm-external-compilation + :active (and coq-compile-before-require + (not (equal coq-compile-command ""))) + :help "Confirm external compilation command, see `coq-compile-command'."] + ["Abort Background Compilation" + coq-par-emergency-cleanup + :active (and coq-compile-before-require + coq-compile-parallel-in-background) + :help "Abort background compilation and kill all compilation processes."]) "" ["Print..." coq-Print :help "With prefix arg (C-u): Set Printing All first"] ["Check..." coq-Check :help "With prefix arg (C-u): Set Printing All first"] |