From e454ae013827b98b814c99ffbc1ca7f2525fb030 Mon Sep 17 00:00:00 2001
From: Hendrik Tews
Date: Sun, 14 Mar 2021 23:07:37 +0100
Subject: 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.
---
 generic/proof-menu.el | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'generic/proof-menu.el')

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
-- 
cgit v1.2.3