Auto-Update {userman, adaptingman}

href: ProofGeneral/PG@c6b7d50

doc/master/adaptingman/Beginning-with-a-New-Prover.html

@@ -258,7 +258,7 @@ <h2 class="section">1.3 Major modes used by Proof General</h2>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>January 22, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>January 23, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 

doc/master/adaptingman/Concept-Index.html

@@ -141,7 +141,7 @@ <h1 class="unnumbered">Concept Index</h1>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>January 22, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>January 23, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 

doc/master/adaptingman/Configuring-Editing-Syntax.html

@@ -86,7 +86,7 @@ <h1 class="chapter">9. Configuring Editing Syntax</h1>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>January 22, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>January 23, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 

doc/master/adaptingman/Configuring-Font-Lock.html

@@ -104,7 +104,7 @@ <h1 class="chapter">10. Configuring Font Lock</h1>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>January 22, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>January 23, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 

doc/master/adaptingman/Configuring-Proof_002dTree-Visualization.html

@@ -507,7 +507,7 @@ <h3 class="subsection">12.4.2 Prooftree Adaption</h3>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>January 22, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>January 23, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 

doc/master/adaptingman/Configuring-Tokens.html

@@ -78,7 +78,7 @@ <h1 class="chapter">11. Configuring Tokens</h1>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>January 22, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>January 23, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 

doc/master/adaptingman/Demonstration-Instantiations.html

@@ -261,7 +261,7 @@ <h2 class="section">B.2 demoisa.el</h2>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>January 22, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>January 23, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 

doc/master/adaptingman/Function-Index.html

@@ -104,7 +104,7 @@ <h1 class="unnumbered">Function and Command Index</h1>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>January 22, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>January 23, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 

doc/master/adaptingman/Global-Constants.html

@@ -55,7 +55,7 @@ <h1 class="chapter">7. Global Constants</h1>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>January 22, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>January 23, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 

doc/master/adaptingman/Goals-Buffer-Settings.html

@@ -102,7 +102,7 @@ <h1 class="chapter">5. Goals Buffer Settings</h1>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>January 22, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>January 23, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 

doc/master/adaptingman/Handling-Multiple-Files.html

@@ -190,7 +190,7 @@ <h1 class="chapter">8. Handling Multiple Files</h1>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>January 22, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>January 23, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 

doc/master/adaptingman/Internals-of-Proof-General.html

@@ -1256,7 +1256,7 @@ <h2 class="section">14.7 Debugging</h2>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>January 22, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>January 23, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 

doc/master/adaptingman/Introduction.html

@@ -121,7 +121,7 @@ <h2 class="unnumberedsec">Credits</h2>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>January 22, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>January 23, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 

doc/master/adaptingman/Menus-and-Toolbar-and-User_002dlevel-Commands.html

@@ -179,7 +179,7 @@ <h2 class="section">2.3 Toolbar configuration</h2>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>January 22, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>January 23, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 

doc/master/adaptingman/PG-adapting_abt.html

@@ -14,7 +14,7 @@
 </div>
 <h1>About This Document</h1>
 <p>
-  This document was generated on <i>January 22, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>January 23, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
 </p>
 <p>
   The buttons in the navigation panels have the following meaning:
@@ -124,7 +124,7 @@ <h1>About This Document</h1>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>January 22, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>January 23, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 

doc/master/adaptingman/PG-adapting_toc.html

@@ -129,7 +129,7 @@ <h1>Table of Contents</h1>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>January 22, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>January 23, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 

doc/master/adaptingman/Plans-and-Ideas.html

@@ -167,7 +167,7 @@ <h2 class="section">A.3 Browser mode for script files and theories</h2>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>January 22, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>January 23, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 

doc/master/adaptingman/Proof-Script-Settings.html

@@ -567,6 +567,21 @@ <h2 class="section">3.6 Omitting proofs for speed</h2>
 displayed and omitting proofs stops at that location for the
 currently asserted region.
 </p>
+<p>In Coq, commands with non-local effects, such as <code>Hint</code>, may
+appear inside proofs. Additionally, admitting a proof of a <code>Let</code>
+declaration causes a warning in Coq. To treat such cases, the
+predicate <code>proof-script-cmd-prevents-proof-omission</code> is applied
+to all commands inside proofs and the regular expression
+<code>proof-script-cmd-force-next-proof-kept</code> is matched against all
+commands outside proofs. In case of a hit, the current or,
+respectively, the next proof is treated as non-opaque and is not
+omitted. Note that a match of
+<code>proof-script-cmd-force-next-proof-kept</code> is only handled if the
+matching command and the following proof appear in the same asserted
+region. If the proof is asserted separately, the information about the
+match in the previously asserted region is lost and the proof may thus
+be omitted.
+</p>
 <p>To enable the omit proofs feature, the following settings must be
 configured.
 </p>
@@ -634,6 +649,35 @@ <h2 class="section">3.6 Omitting proofs for speed</h2>
 <dt><a class="anchor" id="index-proof_002dscript_002dproof_002dadmit_002dcommand"></a><u>Variable:</u> <b>proof-script-proof-admit-command</b></dt>
 <dd><p>Proof command to be inserted instead of omitted proofs.
 </p></dd></dl>
+
+<dl>
+<dt><a class="anchor" id="index-proof_002dscript_002dcmd_002dprevents_002dproof_002domission"></a><u>Variable:</u> <b>proof-script-cmd-prevents-proof-omission</b></dt>
+<dd><p>Optional predicate to match commands that prevent omitting the current proof.<br>
+If set, this option should contain a function that takes a proof
+command (as string) as argument and returns t or nil. If set, the
+function is called on every proof command inside a proof while
+scanning for proofs to omit. The predicate should return t if the
+command has effects ouside the proof, potentially breaking the
+script if the current proof is omitted. If the predicate returns
+t, the proof is considered to be not opaque and thus not omitted.
+</p></dd></dl>
+
+<dl>
+<dt><a class="anchor" id="index-proof_002dscript_002dcmd_002dforce_002dnext_002dproof_002dkept"></a><u>Variable:</u> <b>proof-script-cmd-force-next-proof-kept</b></dt>
+<dd><p>Optional regexp for commands that prevent omitting the next proof.<br>
+If set, this option should contain a regular expression that
+matches proof-script commands that prevent the omission of proofs
+dirctly following this command. When scanning the newly asserted
+region for proofs to omit, every proof-script command outside
+proofs is matched against this regexp. If it matches and the next
+command matches &lsquo;<samp><code>proof-script-proof-start-regexp</code></samp>&rsquo; this following
+proof will not be omitted.
+</p>
+<p>Note that recognition of commands with this regular expression
+does only work if the command and the following proof are
+asserted together.
+</p></dd></dl>
+
 <hr size="6">
 <a class="anchor" id="Safe-_0028state_002dpreserving_0029-commands"></a>
 <a class="anchor" id="Safe-_0028state_002dpreserving_0029-commands-1"></a>
@@ -799,7 +843,7 @@ <h2 class="section">3.11 Completions</h2>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>January 22, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>January 23, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 

doc/master/adaptingman/Proof-Shell-Settings.html

@@ -748,7 +748,7 @@ <h2 class="section">4.5 Hooks and other settings</h2>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>January 22, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>January 23, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 

doc/master/adaptingman/Splash-Screen-Settings.html

@@ -55,7 +55,7 @@ <h1 class="chapter">6. Splash Screen Settings</h1>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>January 22, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>January 23, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 

doc/master/adaptingman/Variable-Index.html

@@ -119,6 +119,8 @@ <h1 class="unnumbered">Variable and User Option Index</h1>
 <tr><td></td><td valign="top"><a href="/doc/master/adaptingman/Proof-Script-Settings#index-proof_002dsave_002dcommand_002dregexp"><code>proof-save-command-regexp</code></a></td><td valign="top"><a href="/doc/master/adaptingman/Proof-Script-Settings#Recognizing-proofs">3.2 Recognizing proofs</a></td></tr>
 <tr><td></td><td valign="top"><a href="/doc/master/adaptingman/Proof-Script-Settings#index-proof_002dsave_002dwith_002dhole_002dregexp"><code>proof-save-with-hole-regexp</code></a></td><td valign="top"><a href="/doc/master/adaptingman/Proof-Script-Settings#Recognizing-proofs">3.2 Recognizing proofs</a></td></tr>
 <tr><td></td><td valign="top"><a href="/doc/master/adaptingman/Internals-of-Proof-General#index-proof_002dscript_002dbuffer"><code>proof-script-buffer</code></a></td><td valign="top"><a href="/doc/master/adaptingman/Internals-of-Proof-General#Global-variables">14.4 Global variables</a></td></tr>
+<tr><td></td><td valign="top"><a href="/doc/master/adaptingman/Proof-Script-Settings#index-proof_002dscript_002dcmd_002dforce_002dnext_002dproof_002dkept"><code>proof-script-cmd-force-next-proof-kept</code></a></td><td valign="top"><a href="/doc/master/adaptingman/Proof-Script-Settings#Omitting-proofs-for-speed">3.6 Omitting proofs for speed</a></td></tr>
+<tr><td></td><td valign="top"><a href="/doc/master/adaptingman/Proof-Script-Settings#index-proof_002dscript_002dcmd_002dprevents_002dproof_002domission"><code>proof-script-cmd-prevents-proof-omission</code></a></td><td valign="top"><a href="/doc/master/adaptingman/Proof-Script-Settings#Omitting-proofs-for-speed">3.6 Omitting proofs for speed</a></td></tr>
 <tr><td></td><td valign="top"><a href="/doc/master/adaptingman/Proof-Script-Settings#index-proof_002dscript_002dcommand_002dend_002dregexp"><code>proof-script-command-end-regexp</code></a></td><td valign="top"><a href="/doc/master/adaptingman/Proof-Script-Settings#Recognizing-commands-and-comments">3.1 Recognizing commands and comments</a></td></tr>
 <tr><td></td><td valign="top"><a href="/doc/master/adaptingman/Proof-Script-Settings#index-proof_002dscript_002dcommand_002dstart_002dregexp"><code>proof-script-command-start-regexp</code></a></td><td valign="top"><a href="/doc/master/adaptingman/Proof-Script-Settings#Recognizing-commands-and-comments">3.1 Recognizing commands and comments</a></td></tr>
 <tr><td></td><td valign="top"><a href="/doc/master/adaptingman/Proof-Script-Settings#index-proof_002dscript_002dcomment_002dend"><code>proof-script-comment-end</code></a></td><td valign="top"><a href="/doc/master/adaptingman/Proof-Script-Settings#Recognizing-commands-and-comments">3.1 Recognizing commands and comments</a></td></tr>
@@ -235,7 +237,7 @@ <h1 class="unnumbered">Variable and User Option Index</h1>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>January 22, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>January 23, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 

doc/master/adaptingman/Writing-More-Lisp-Code.html

@@ -248,7 +248,7 @@ <h2 class="section">13.4 Useful functions and macros</h2>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>January 22, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>January 23, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 

doc/master/adaptingman/index.html

@@ -80,7 +80,7 @@ <h1 class="settitle">Proof General</h1>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>January 22, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>January 23, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 

doc/master/userman/Advanced-Script-Management-and-Editing.html

@@ -550,7 +550,7 @@ <h2 class="section">3.10 Editing features</h2>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>January 22, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>January 23, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 

doc/master/userman/Basic-Script-Management.html

@@ -711,17 +711,32 @@ <h2 class="section">2.6 Script processing commands</h2>
 proof is opaque, if its proof script or proof term cannot
 influence the following code. In Coq, opaque proofs are finished
 with <code>Qed</code>, non-opaque ones with <code>Defined</code>. When this
-omit proofs feature is configured, complete opaque proofs are
-silently replace with a suitable cheating command
+omit-proofs feature is configured, complete opaque proofs are
+silently replaced with a suitable cheating command
 (<code>Admitted</code> for Coq) before sending the proof to the proof
 assistant. For files with big proofs this can bring down the
 processing time to 10% with the obvious disadvantage that errors
-in the omitted proofs go unnoticed. For checking the proofs
-occasionally, a prefix argument for <code>proof-goto-point</code> and
-<code>proof-process-buffer</code> causes these commands to disregard
-the setting of <code>proof-omit-proofs-option</code>. Currently, the
-omit proofs feature is only supported for Coq.
-</li><li>
+in the omitted proofs go unnoticed. Currently, the omit-proofs
+feature is only supported for Coq.
+
+<p>A prefix argument for <code>proof-goto-point</code> and
+<code>proof-process-buffer</code> toggles the omit-proofs feature
+temporarily for this invocation. That is, if
+<code>proof-omit-proofs-option</code> has been set to <code>t</code>, a prefix
+argument switches the omit-proofs feature off for these commands. Vice
+versa, if <code>proof-omit-proofs-option</code> is <code>nil</code>, a prefix
+argument switches the omit-proofs feature temporarily on for one
+invocation.
+</p>
+<p>Note that the omit-proof feature works by examining the asserted
+region with different regular expressions to recognize proofs and to
+differentiate opaque from non-opaque proofs. This approach is
+necessarily imprecise and it may happen that certain non-opaque proofs
+are classified as opaque ones, thus being omitted and that the proof
+script therefore fails unexpectedly at a later point. Therefore, if a
+proof script fails unexpectedly try processing it again after
+disabling the omit-proofs feature.
+</p></li><li>
 An often used poor man&rsquo;s solution is to collect all new material
 at the end of one file, regardless where the material really
 belongs. When the final theorem has been proved, one cleans up
@@ -1094,7 +1109,7 @@ <h2 class="section">2.9 Interrupting during trace output</h2>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>January 22, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>January 23, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 

doc/master/userman/Bugs-and-Enhancements.html

@@ -50,7 +50,7 @@ <h1 class="appendix">B. Bugs and Enhancements</h1>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>January 22, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>January 23, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>