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-faces.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-faces.el')
| -rw-r--r-- | generic/proof-faces.el | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/generic/proof-faces.el b/generic/proof-faces.el index 115d8667..b06a64fd 100644 --- a/generic/proof-faces.el +++ b/generic/proof-faces.el @@ -218,6 +218,13 @@ Warning messages can come from proof assistant or from Proof General itself." "Proof General face for highlighting an error in the proof script. " :group 'proof-faces) +(defface proof-omitted-proof-face + (proof-face-specs + (:background "#EAEFFF" :extend t) + (:background "#9C4A90" :extend t) + (:foreground "white" :background "black" :extend t)) + "*Face for background of omitted proofs" + :group 'proof-faces) ;;; Compatibility: these are required for use in GNU Emacs/font-lock-keywords |