diff options
| author | Hendrik Tews | 2021-03-17 08:37:38 +0100 |
|---|---|---|
| committer | Hendrik Tews | 2021-04-16 22:53:05 +0200 |
| commit | f7943ba646c258a0a4a5b397b8a920d5d13ecf31 (patch) | |
| tree | 26647718255a8a6f04f51123fe9e67ec0255603a /doc/ProofGeneral.texi | |
| parent | e454ae013827b98b814c99ffbc1ca7f2525fb030 (diff) | |
prefix arg for temporarily disabling omitting proofs
Make proof-goto-point and proof-process-buffer prefix argument
aware. With argument, both commands temporarily switch off
proof-omit-proofs-option, such that all proofs are completely
processed for one particular invocation.
Diffstat (limited to 'doc/ProofGeneral.texi')
| -rw-r--r-- | doc/ProofGeneral.texi | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index beb5cc9f..49275d64 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -1522,15 +1522,19 @@ deleted text. @c TEXI DOCSTRING MAGIC: proof-goto-point -@deffn Command proof-goto-point +@deffn Command proof-goto-point &optional raw Assert or retract to the command at current position.@* Calls @samp{@code{proof-assert-until-point}} or @samp{@code{proof-retract-until-point}} as -appropriate. +appropriate. With prefix argument @var{raw} the omit proofs feature +(@samp{@code{proof-omit-proofs-option}}) is temporaily disabled to check all +proofs in the asserted region. @end deffn @c TEXI DOCSTRING MAGIC: proof-process-buffer -@deffn Command proof-process-buffer -Process the current (or script) buffer, and maybe move point to the end. +@deffn Command proof-process-buffer &optional raw +Process the current (or script) buffer, and maybe move point to the end.@* +With prefix argument @var{raw} the omit proofs feature (@samp{@code{proof-omit-proofs-option}}) +is temporaily disabled to check all proofs in the asserted region. @end deffn @c TEXI DOCSTRING MAGIC: proof-retract-buffer |