branch: elpa/proof-general
commit 265ce5cc5f161c6c81b3c42123ac15b574519a4f
Author: Hendrik Tews <[email protected]>
Commit: hendriktews <[email protected]>
proof-stat: add menu item for proof-check-proofs
---
doc/ProofGeneral.texi | 34 ++++++++++++++++++----------------
generic/proof-menu.el | 6 +++++-
2 files changed, 23 insertions(+), 17 deletions(-)
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 9520d5cc33..de74c7c1d5 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -2261,12 +2261,13 @@ the proof assistant to automatically process other
files.
@section Proof status statistic
@cindex Proof status statistic
-The command @code{proof-check-proofs} generates the proof status of
-all opaque proofs in the current buffer, i.e., it generates an
-overview that shows which of the opaque proofs in the current buffer
-are currently valid and which are failing. When used interactively,
-the proof status is shown in the buffer @code{*proof-check-report*}
-(as long as @code{proof-check-report-buffer} is not changed).
+The command @code{proof-check-proofs} (menu @code{Proof-General ->
+Check Opaque Proofs}) generates the proof status of all opaque proofs
+in the current buffer, i.e., it generates an overview that shows which
+of the opaque proofs in the current buffer are currently valid and
+which are failing. When used interactively, the proof status is shown
+in the buffer @code{*proof-check-report*} (as long as
+@code{proof-check-report-buffer} is not changed).
Currently @code{proof-check-proofs} does only work for Coq.
@@ -2314,7 +2315,7 @@ omit-proofs feature.
The interactive use of this commands is limited because it only works
on the current buffer. However, this commands can also be run in batch
mode in a script, for instance in a continuous integration
-environment. To run this command on a buffer in batch mode, use
+environment. To run this command on a file in batch mode, use
@verbatim
emacs -batch -l <your-pg-dir>/generic/proof-site.el <file> \
@@ -5252,15 +5253,16 @@ non-opaque, even if they have proof-local effect only,
such as
@node Proof status statistic for Coq
@section Proof status statistic for Coq
-The command @code{proof-check-proofs} generates the proof status of
-all opaque proofs in the current buffer, i.e., it generates an
-overview that shows which of the opaque proofs in the current buffer
-are currently valid and which are failing. This command is useful for
-a development process where invalid proofs are permitted and vos
-compilation (@xref{Quick and inconsistent compilation}) and the omit
-proofs feature (@xref{Omitting proofs for speed}) are used to work at
-the most interesting or challenging point instead of on the first
-invalid proof. See @xref{Proof status statistic} for more details.
+The command @code{proof-check-proofs} (menu @code{Proof-General ->
+Check Opaque Proofs}) generates the proof status of all opaque proofs
+in the current buffer, i.e., it generates an overview that shows which
+of the opaque proofs in the current buffer are currently valid and
+which are failing. This command is useful for a development process
+where invalid proofs are permitted and vos compilation (@xref{Quick
+and inconsistent compilation}) and the omit proofs feature
+(@xref{Omitting proofs for speed}) are used to work at the most
+interesting or challenging point instead of on the first invalid
+proof. See @xref{Proof status statistic} for more details.
@node Editing multiple proofs
diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index 77bc05a84b..35f6741a93 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -702,7 +702,11 @@ without adjusting window layout."
:active pg-next-error-regexp]
["Scripting Active" proof-toggle-active-scripting
:style toggle
- :selected (eq proof-script-buffer (current-buffer))])
+ :selected (eq proof-script-buffer (current-buffer))]
+ ["Check Opaque Proofs" proof-check-proofs
+ :active (and proof-omit-proofs-configured
+ proof-get-proof-info-fn
+ proof-retract-command-fn)])
"The Proof General generic menu for scripting buffers.")
