aboutsummaryrefslogtreecommitdiff
path: root/generic/proof-menu.el
diff options
context:
space:
mode:
authorErik Martin-Dorel2021-04-21 20:00:36 +0200
committerGitHub2021-04-21 20:00:36 +0200
commitb5c4c3a1423c7925194334d66c262054d6a6c4c5 (patch)
treee7878c97ece66bd7941e8f6019f70325de3f1bd1 /generic/proof-menu.el
parentd0acb626eba17023c55b002921870d60e48527a5 (diff)
parent82311da10ee3dfa6f29ddfb9225f9f05c29dca31 (diff)
Merge pull request #559 from hendriktews/omit-proofsHEADmaster
Add feature to omit complete opaque proofs
Diffstat (limited to 'generic/proof-menu.el')
-rw-r--r--generic/proof-menu.el6
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