Auto-Update {userman, adaptingman}

href: ProofGeneral/PG@f5d929e

Author: proofbot

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>May 13, 2025</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 16, 2025</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>May 13, 2025</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 16, 2025</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>May 13, 2025</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 16, 2025</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>May 13, 2025</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 16, 2025</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

@@ -20,7 +20,7 @@
 <h1 class="chapter">12. Configuring Proof-Tree Visualization</h1>
 
 <p><b>Parts of this section are outdated. Please create an issue at
-github.com/ProofGeneral/Proof General if you have a question for
+github.com/ProofGeneral/PG if you have a question for
 adapting Prooftree for a new proof assistant.</b>
 </p>
 <p>The proof-tree visualization feature was written with the idea of
@@ -311,28 +311,25 @@ <h3 class="subsection">12.3.4 Urgent and Delayed Actions</h3>
 speed, the amount of urgent code should be kept small.
 </p>
 <dl>
-<dt><a class="anchor" id="index-proof_002dtree_002dcheck_002dproof_002dfinish"></a><u>Function:</u> <b>proof-tree-check-proof-finish</b><i> last-item</i></dt>
-<dd><p>Urgent action to delay processing at proof end.<br>
-This function is called from &lsquo;<samp><code>proof-shell-exec-loop</code></samp>&rsquo; after the
-old item has been removed and before the next item from
-&lsquo;<samp><code>proof-action-list</code></samp>&rsquo; is sent to the proof assistant. Of course
-only when the proof-tree display is active. At the end of the
-proof, this function delays items just following the previous
-proof until all show-goal commands from prooftree and the
-&lsquo;<samp><code>proof-tree-display-stop-command</code></samp>&rsquo; (which switches the dependent
-evar line off for Coq) have been processed.
-</p>
-<p>If this function detects the end of the proof, it moves
-non-priority items following in &lsquo;<samp><code>proof-action-list</code></samp>&rsquo; to
-&lsquo;<samp><code>proof-tree--delayed-actions</code></samp>&rsquo; and sets
-&lsquo;<samp><code>proof-second-action-list-active</code></samp>&rsquo;. When later the command from
-&lsquo;<samp><code>proof-tree-display-stop-command</code></samp>&rsquo; is recognized, the items are
-moved back. If no items follow the end of the previous proof,
-&lsquo;<samp><code>proof-tree-display-stop-command</code></samp>&rsquo; is set to t.
+<dt><a class="anchor" id="index-proof_002dtree_002durgent_002daction"></a><u>Function:</u> <b>proof-tree-urgent-action</b><i> last-item</i></dt>
+<dd><p>Urgent actions for proof-tree display.<br>
+This is the second entry point of the Proof General prooftree support,
+see also &lsquo;<samp><code>proof-tree-handle-delayed-output</code></samp>&rsquo;. Call
+&lsquo;<samp><code>proof-tree-check-proof-finish</code></samp>&rsquo; to delay processing the queue region at
+the end of a proof until all show-goal commands from prooftree have been
+processed. Do also call &lsquo;<samp><code>proof-tree-assistant-specific-urgent-action</code></samp>&rsquo;,
+which appropriately inserts show-goal commands if Coq is running
+completely silent. <var>last-item</var> is the last proof-action item that has just
+been processed.
+</p>
+<p>When the proof-tree display is active, this function is called from
+&lsquo;<samp><code>proof-shell-exec-loop</code></samp>&rsquo; after the old item has been removed and before
+the next item from &lsquo;<samp><code>proof-action-list</code></samp>&rsquo; is sent to the proof assistant.
+At this place &lsquo;<samp><code>proof-action-list</code></samp>&rsquo; can be directly manipulated.
 </p></dd></dl>
 
 
-<p>The function <code>proof-tree-check-proof-finish</code> is called at a point
+<p>The function <code>proof-tree-urgent-action</code> is called at a point
 where it is save to manipulate <code>proof-action-list</code>. This is
 essential, because <code>proof-tree-urgent-action</code> inserts goal
 display commands into <code>proof-action-list</code> when existential
@@ -347,9 +344,10 @@ <h3 class="subsection">12.3.4 Urgent and Delayed Actions</h3>
 <dl>
 <dt><a class="anchor" id="index-proof_002dtree_002dhandle_002ddelayed_002doutput"></a><u>Function:</u> <b>proof-tree-handle-delayed-output</b><i> old-proof-marker cmd flags _span</i></dt>
 <dd><p>Process delayed output for prooftree.<br>
-This function is the main entry point of the Proof General
-prooftree support.  It examines the delayed output in order to
-take appropriate actions and maintains the internal state.
+This function is the main entry point of the Proof General prooftree
+support, but see also &lsquo;<samp><code>proof-tree-urgent-action</code></samp>&rsquo;. It examines the
+delayed output in order to take appropriate actions and maintains the
+internal state.
 </p>
 <p>The delayed output to handle is in the region
 [<code>proof-shell-delayed-output-start</code>, <code>proof-shell-delayed-output-end</code>].
@@ -455,7 +453,7 @@ <h3 class="subsection">12.4.2 Prooftree Adaption</h3>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>May 13, 2025</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 16, 2025</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>May 13, 2025</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 16, 2025</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>May 13, 2025</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 16, 2025</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 

doc/master/adaptingman/Function-Index.html

@@ -79,9 +79,9 @@ <h1 class="unnumbered">Function and Command Index</h1>
 <tr><td></td><td valign="top"><a href="/doc/master/adaptingman/Internals-of-Proof-General#index-proof_002dshell_002dprocess_002durgent_002dmessage"><code>proof-shell-process-urgent-message</code></a></td><td valign="top"><a href="/doc/master/adaptingman/Internals-of-Proof-General#Output-from-the-shell">14.6.2 Output from the shell</a></td></tr>
 <tr><td></td><td valign="top"><a href="/doc/master/adaptingman/Internals-of-Proof-General#index-proof_002dshell_002drestart"><code>proof-shell-restart</code></a></td><td valign="top"><a href="/doc/master/adaptingman/Internals-of-Proof-General#Proof-shell-mode">14.6 Proof shell mode</a></td></tr>
 <tr><td></td><td valign="top"><a href="/doc/master/adaptingman/Internals-of-Proof-General#index-proof_002dshell_002dstart"><code>proof-shell-start</code></a></td><td valign="top"><a href="/doc/master/adaptingman/Internals-of-Proof-General#Proof-shell-mode">14.6 Proof shell mode</a></td></tr>
-<tr><td></td><td valign="top"><a href="/doc/master/adaptingman/Configuring-Proof_002dTree-Visualization#index-proof_002dtree_002dcheck_002dproof_002dfinish"><code>proof-tree-check-proof-finish</code></a></td><td valign="top"><a href="/doc/master/adaptingman/Configuring-Proof_002dTree-Visualization#Urgent-and-Delayed-Actions">12.3.4 Urgent and Delayed Actions</a></td></tr>
 <tr><td></td><td valign="top"><a href="/doc/master/adaptingman/Configuring-Proof_002dTree-Visualization#index-proof_002dtree_002dexternal_002ddisplay_002dtoggle"><code>proof-tree-external-display-toggle</code></a></td><td valign="top"><a href="/doc/master/adaptingman/Configuring-Proof_002dTree-Visualization#Guards">12.3.3 Guards</a></td></tr>
 <tr><td></td><td valign="top"><a href="/doc/master/adaptingman/Configuring-Proof_002dTree-Visualization#index-proof_002dtree_002dhandle_002ddelayed_002doutput"><code>proof-tree-handle-delayed-output</code></a></td><td valign="top"><a href="/doc/master/adaptingman/Configuring-Proof_002dTree-Visualization#Urgent-and-Delayed-Actions">12.3.4 Urgent and Delayed Actions</a></td></tr>
+<tr><td></td><td valign="top"><a href="/doc/master/adaptingman/Configuring-Proof_002dTree-Visualization#index-proof_002dtree_002durgent_002daction"><code>proof-tree-urgent-action</code></a></td><td valign="top"><a href="/doc/master/adaptingman/Configuring-Proof_002dTree-Visualization#Urgent-and-Delayed-Actions">12.3.4 Urgent and Delayed Actions</a></td></tr>
 <tr><td></td><td valign="top"><a href="/doc/master/adaptingman/Configuring-Font-Lock#index-proof_002dzap_002dcommas"><code>proof-zap-commas</code></a></td><td valign="top"><a href="/doc/master/adaptingman/Configuring-Font-Lock#Configuring-Font-Lock">10. Configuring Font Lock</a></td></tr>
 <tr><td colspan="3"> <hr></td></tr>
 </table>
@@ -104,7 +104,7 @@ <h1 class="unnumbered">Function and Command Index</h1>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>May 13, 2025</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 16, 2025</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>May 13, 2025</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 16, 2025</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>May 13, 2025</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 16, 2025</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>