diff options
| author | Hendrik Tews | 2021-03-14 23:07:37 +0100 |
|---|---|---|
| committer | Hendrik Tews | 2021-04-16 22:53:05 +0200 |
| commit | e454ae013827b98b814c99ffbc1ca7f2525fb030 (patch) | |
| tree | e4df56200641e8c235a180aa86bb68392c7e1f45 /generic/proof-menu.el | |
| parent | f0f0476d07401aba2cf428a71f7ee960cd1b3154 (diff) | |
add feature to omit complete opaque proofs
This commit adds a feature to recognize complete opaque proofs in
the asserted region and to replace them with an admitted proof.
This can drastically improve the processing time for the asserted
region at the cost of not checking the omitted proofs. Omitted
proofs are displayed slightly darker compared to other parts of
the locked region.
With this commit, the feature is supported for Coq for files in
which proofs are started with some form of Proof and ended with
either Qed, Defined, Admitted or Abort.
To enable, configure proof-omit-proofs-option or click
Proof General -> Quick Options -> Processing -> Omit Proofs.
Diffstat (limited to 'generic/proof-menu.el')
| -rw-r--r-- | generic/proof-menu.el | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/generic/proof-menu.el b/generic/proof-menu.el index 3846229e..e15ce4d5 100644 --- a/generic/proof-menu.el +++ b/generic/proof-menu.el @@ -334,6 +334,7 @@ without adjusting window layout." (proof-deftoggle proof-fast-process-buffer) (proof-deftoggle proof-imenu-enable proof-imenu-toggle) (proof-deftoggle proof-keep-response-history) +(proof-deftoggle proof-omit-proofs-option) (proof-eval-when-ready-for-assistant ;; togglers for settings separately configurable per-prover @@ -361,6 +362,11 @@ without adjusting window layout." ;;; :selected proof-keep-response-history] ("Processing" + ["Omit Proofs" proof-omit-proofs-option-toggle + :style toggle + :selected proof-omit-proofs-option + :active proof-omit-proofs-configured + :help "Skip over proofs, admitting theorems, when asserting larger chunks"] ["Fast Process Buffer" proof-fast-process-buffer-toggle :style toggle :selected proof-fast-process-buffer |