Auto-Update {userman, adaptingman}

href: ProofGeneral/PG@75c13f9

Author: proofbot

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

@@ -96,9 +96,9 @@ <h2 class="section">1.1 Overview of adding a new prover</h2>
 <dl>
 <dt><a class="anchor" id="index-proof_002dassistant_002dtable"></a><u>Variable:</u> <b>proof-assistant-table</b></dt>
 <dd><p>Proof General&rsquo;s table of supported proof assistants.<br>
-This is copied from &lsquo;<samp><code>proof-assistant-table-default</code></samp>&rsquo; at load time,
+This is copied from <code>proof-assistant-table-default</code> at load time,
 removing any entries that do not have a corresponding directory
-under &lsquo;<samp><code>proof-home-directory</code></samp>&rsquo;.
+under <code>proof-home-directory</code>.
 </p>
 <p>Each entry is a list of the form
 </p><table><tr><td>&nbsp;</td><td><pre class="lisp">  (<var>symbol</var> <var>name</var> <var>file-extension</var> [AUTOMODE-REGEXP] [IGNORED-EXTENSIONS-LIST])
@@ -109,14 +109,14 @@ <h2 class="section">1.1 Overview of adding a new prover</h2>
 (or with extension <var>file-extension</var>) are visited.  If present,
 <var>ignored-extensions-list</var> is a list of file-name extensions to be
 ignored when doing file-name completion (<var>ignored-extensions-list</var>
-is added to &lsquo;<samp><code>completion-ignored-extensions</code></samp>&rsquo;).
+is added to <code>completion-ignored-extensions</code>).
 </p>
 <p><var>symbol</var> is also used to form the name of the directory and elisp
 file for the mode, which will be
 </p><table><tr><td>&nbsp;</td><td><pre class="lisp">    <var>proof-home-directory</var>/<var>symbol</var>/<var>symbol</var>.el
 </pre></td></tr></table>
 <p>where <var>proof-home-directory</var> is the value of the
-variable &lsquo;<samp><code>proof-home-directory</code></samp>&rsquo;.
+variable <code>proof-home-directory</code>.
 </p></dd></dl>
 
 
@@ -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 13, 2026</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>January 24, 2026</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 13, 2026</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>January 24, 2026</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 

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

@@ -35,21 +35,21 @@ <h1 class="chapter">9. Configuring Editing Syntax</h1>
 A flat list of the form
 </p><table><tr><td>&nbsp;</td><td><pre class="lisp">  (<var>char</var> <var>syncode</var> <var>char</var> <var>syncode</var> ...)
 </pre></td></tr></table>
-<p>See doc of &lsquo;<samp><code>modify-syntax-entry</code></samp>&rsquo; for details of characters
+<p>See doc of <code>modify-syntax-entry</code> for details of characters
 and syntax codes.
 </p>
-<p>At present this is used only by the &lsquo;<samp><code>proof-easy-config</code></samp>&rsquo; macro.
+<p>At present this is used only by the <code>proof-easy-config</code> macro.
 </p></dd></dl>
 <dl>
 <dt><a class="anchor" id="index-proof_002dshell_002dsyntax_002dtable_002dentries"></a><u>Variable:</u> <b>proof-shell-syntax-table-entries</b></dt>
 <dd><p>List of syntax table entries for proof script mode.<br>
 A flat list of the form
 </p><table><tr><td>&nbsp;</td><td><pre class="lisp">  (<var>char</var> <var>syncode</var> <var>char</var> <var>syncode</var> ...)
 </pre></td></tr></table>
-<p>See doc of &lsquo;<samp><code>modify-syntax-entry</code></samp>&rsquo; for details of characters
+<p>See doc of <code>modify-syntax-entry</code> for details of characters
 and syntax codes.
 </p>
-<p>At present this is used only by the &lsquo;<samp><code>proof-easy-config</code></samp>&rsquo; macro.
+<p>At present this is used only by the <code>proof-easy-config</code> macro.
 </p></dd></dl>
 <p>Some additional useful settings are:
 </p>
@@ -86,7 +86,7 @@ <h1 class="chapter">9. Configuring Editing Syntax</h1>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>January 13, 2026</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>January 24, 2026</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 

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

@@ -38,24 +38,24 @@ <h1 class="chapter">10. Configuring Font Lock</h1>
 </p>
 <dl>
 <dt><a class="anchor" id="index-proof_002dscript_002dfont_002dlock_002dkeywords"></a><u>Variable:</u> <b>proof-script-font-lock-keywords</b></dt>
-<dd><p>Value of &lsquo;<samp><code>font-lock-keywords</code></samp>&rsquo; used to fontify proof scripts.<br>
-The proof script mode should set this before calling &lsquo;<samp><code>proof-config-done</code></samp>&rsquo;.
-Used also by &lsquo;<samp><code>proof-easy-config</code></samp>&rsquo; mechanism.
-See also &lsquo;<samp><code>proof-goals-font-lock-keywords</code></samp>&rsquo; and &lsquo;<samp><code>proof-response-font-lock-keywords</code></samp>&rsquo;.
+<dd><p>Value of <code>font-lock-keywords</code> used to fontify proof scripts.<br>
+The proof script mode should set this before calling <code>proof-config-done</code>.
+Used also by <code>proof-easy-config</code> mechanism.
+See also <code>proof-goals-font-lock-keywords</code> and <code>proof-response-font-lock-keywords</code>.
 </p></dd></dl>
 <dl>
 <dt><a class="anchor" id="index-proof_002dgoals_002dfont_002dlock_002dkeywords"></a><u>Variable:</u> <b>proof-goals-font-lock-keywords</b></dt>
-<dd><p>Value of &lsquo;<samp><code>font-lock-keywords</code></samp>&rsquo; used to fontify the goals output.<br>
-The goals shell mode should set this before calling &lsquo;<samp><code>proof-goals-config-done</code></samp>&rsquo;.
-Used also by &lsquo;<samp><code>proof-easy-config</code></samp>&rsquo; mechanism.
-See also &lsquo;<samp><code>proof-script-font-lock-keywords</code></samp>&rsquo; and &lsquo;<samp><code>proof-response-font-lock-keywords</code></samp>&rsquo;.
+<dd><p>Value of <code>font-lock-keywords</code> used to fontify the goals output.<br>
+The goals shell mode should set this before calling <code>proof-goals-config-done</code>.
+Used also by <code>proof-easy-config</code> mechanism.
+See also <code>proof-script-font-lock-keywords</code> and <code>proof-response-font-lock-keywords</code>.
 </p></dd></dl>
 <dl>
 <dt><a class="anchor" id="index-proof_002dresponse_002dfont_002dlock_002dkeywords"></a><u>Variable:</u> <b>proof-response-font-lock-keywords</b></dt>
-<dd><p>Value of &lsquo;<samp><code>font-lock-keywords</code></samp>&rsquo; used to fontify the response output.<br>
-The response mode should set this before calling &lsquo;<samp><code>proof-response-config-done</code></samp>&rsquo;.
-Used also by &lsquo;<samp><code>proof-easy-config</code></samp>&rsquo; mechanism.
-See also &lsquo;<samp><code>proof-script-font-lock-keywords</code></samp>&rsquo; and &lsquo;<samp><code>proof-goals-font-lock-keywords</code></samp>&rsquo;.
+<dd><p>Value of <code>font-lock-keywords</code> used to fontify the response output.<br>
+The response mode should set this before calling <code>proof-response-config-done</code>.
+Used also by <code>proof-easy-config</code> mechanism.
+See also <code>proof-script-font-lock-keywords</code> and <code>proof-goals-font-lock-keywords</code>.
 </p></dd></dl>
 <p>Proof General provides a special function, <code>proof-zap-commas</code>, for
 tweaking the font lock behaviour of provers which have declarations of
@@ -68,7 +68,7 @@ <h1 class="chapter">10. Configuring Font Lock</h1>
 <dl>
 <dt><a class="anchor" id="index-proof_002dzap_002dcommas"></a><u>Function:</u> <b>proof-zap-commas</b><i> limit</i></dt>
 <dd><p>Remove the face of all &lsquo;<samp>,</samp>&rsquo; from point to <var>limit</var>.<br>
-Meant to be used from &lsquo;<samp><code>font-lock-keywords</code></samp>&rsquo; as a way
+Meant to be used from <code>font-lock-keywords</code> as a way
 to unfontify commas in declarations and definitions.
 Useful for provers which have declarations of the form x,y,z:Ty
 All that can be said for it is that the previous ways of doing
@@ -79,7 +79,7 @@ <h1 class="chapter">10. Configuring Font Lock</h1>
 <dt><a class="anchor" id="index-pg_002dbefore_002dfontify_002doutput_002dhook"></a><u>Variable:</u> <b>pg-before-fontify-output-hook</b></dt>
 <dd><p>This hook is called before fontifying a region in an output buffer.<br>
 A function on this hook can alter the region of the buffer within
-the current restriction, and must return the final value of (<code>point-max</code>).
+the current restriction, and must return the final value of <code>point-max</code>.
 [This hook is presently only used by phox-sym-lock].
 </p></dd></dl>
 
@@ -104,7 +104,7 @@ <h1 class="chapter">10. Configuring Font Lock</h1>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>January 13, 2026</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>January 24, 2026</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

@@ -266,7 +266,7 @@ <h3 class="subsection">12.3.3 Guards</h3>
 display.  In this case, this variable stays t and the proof-tree
 display will be started for the next proof.
 </p>
-<p>Controlled by &lsquo;<samp><code>proof-tree-external-display-toggle</code></samp>&rsquo;.
+<p>Controlled by <code>proof-tree-external-display-toggle</code>.
 </p></dd></dl>
 
 <p>In Proof General, the code for the external proof-tree display is
@@ -314,18 +314,18 @@ <h3 class="subsection">12.3.4 Urgent and Delayed Actions</h3>
 <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
+see also <code>proof-tree-handle-delayed-output</code>.  Call
+<code>proof-tree-check-proof-finish</code> 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;,
+processed.  Do also call <code>proof-tree-assistant-specific-urgent-action</code>,
 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.
+<code>proof-shell-exec-loop</code> after the old item has been removed and before
+the next item from <code>proof-action-list</code> is sent to the proof assistant.
+At this place <code>proof-action-list</code> can be directly manipulated.
 </p></dd></dl>
 
 
@@ -345,17 +345,17 @@ <h3 class="subsection">12.3.4 Urgent and Delayed Actions</h3>
 <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, but see also &lsquo;<samp><code>proof-tree-urgent-action</code></samp>&rsquo;.  It examines the
+support, but see also <code>proof-tree-urgent-action</code>.  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>].
 Urgent messages might be before that, following <var>old-proof-marker</var>,
-which contains the position of &lsquo;<samp><code>proof-marker</code></samp>&rsquo;, before the next
+which contains the position of <code>proof-marker</code>, before the next
 command was sent to the proof assistant.
 </p>
-<p>All other arguments are (former) fields of the &lsquo;<samp><code>proof-action-list</code></samp>&rsquo;
+<p>All other arguments are (former) fields of the <code>proof-action-list</code>
 entry that is now finally retired.  <var>cmd</var> is the command, <var>flags</var> are
 the flags and <var>span</var> is the span.
 </p></dd></dl>
@@ -453,7 +453,7 @@ <h3 class="subsection">12.4.2 Prooftree Adaption</h3>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>January 13, 2026</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>January 24, 2026</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 13, 2026</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>January 24, 2026</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 13, 2026</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>January 24, 2026</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 13, 2026</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>January 24, 2026</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 

doc/master/adaptingman/Global-Constants.html

@@ -37,7 +37,7 @@ <h1 class="chapter">7. Global Constants</h1>
 <dt><a class="anchor" id="index-proof_002duniversal_002dkeys"></a><u>Variable:</u> <b>proof-universal-keys</b></dt>
 <dd><p>List of key bindings made for all proof general buffers.<br>
 Elements of the list are tuples &lsquo;<samp>(k . f)</samp>&rsquo;
-where &lsquo;<samp>k</samp>&rsquo; is a key binding (vector) and &lsquo;<samp>f</samp>&rsquo; the designated function.
+where <code>k</code> is a key binding (vector) and <code>f</code> the designated function.
 </p></dd></dl>
 
 
@@ -55,7 +55,7 @@ <h1 class="chapter">7. Global Constants</h1>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>January 13, 2026</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>January 24, 2026</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 

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

@@ -45,28 +45,28 @@ <h1 class="chapter">5. Goals Buffer Settings</h1>
 <dl>
 <dt><a class="anchor" id="index-proof_002dshell_002dresult_002dstart"></a><u>Variable:</u> <b>proof-shell-result-start</b></dt>
 <dd><p>Regexp matching start of an output from the prover after pbp commands.<br>
-In particular, after a &lsquo;<samp><code>pbp-goal-command</code></samp>&rsquo; or a &lsquo;<samp><code>pbp-hyp-command</code></samp>&rsquo;.
+In particular, after a <code>pbp-goal-command</code> or a <code>pbp-hyp-command</code>.
 </p></dd></dl>
 <dl>
 <dt><a class="anchor" id="index-proof_002dshell_002dresult_002dend"></a><u>Variable:</u> <b>proof-shell-result-end</b></dt>
 <dd><p>Regexp matching end of output from the prover after pbp commands.<br>
-In particular, after a &lsquo;<samp><code>pbp-goal-command</code></samp>&rsquo; or a &lsquo;<samp><code>pbp-hyp-command</code></samp>&rsquo;.
+In particular, after a <code>pbp-goal-command</code> or a <code>pbp-hyp-command</code>.
 </p></dd></dl>
 
 <dl>
 <dt><a class="anchor" id="index-pg_002dsubterm_002dstart_002dchar"></a><u>Variable:</u> <b>pg-subterm-start-char</b></dt>
 <dd><p>Opening special character for subterm markup.<br>
 Subsequent special characters with values <strong>below</strong>
-&lsquo;<samp><code>pg-subterm-first-special-char</code></samp>&rsquo; are assumed to be subterm position
-indicators.  Annotations should be finished with &lsquo;<samp><code>pg-subterm-sep-char</code></samp>&rsquo;;
-the end of the concrete syntax is indicated by &lsquo;<samp><code>pg-subterm-end-char</code></samp>&rsquo;.
+<code>pg-subterm-first-special-char</code> are assumed to be subterm position
+indicators.  Annotations should be finished with <code>pg-subterm-sep-char</code>;
+the end of the concrete syntax is indicated by <code>pg-subterm-end-char</code>.
 </p>
-<p>If &lsquo;<samp><code>pg-subterm-start-char</code></samp>&rsquo; is nil, subterm markup is disabled.
+<p>If <code>pg-subterm-start-char</code> is nil, subterm markup is disabled.
 </p></dd></dl>
 <dl>
 <dt><a class="anchor" id="index-pg_002dsubterm_002dsep_002dchar"></a><u>Variable:</u> <b>pg-subterm-sep-char</b></dt>
 <dd><p>Finishing special for a subterm markup.<br>
-See doc of &lsquo;<samp><code>pg-subterm-start-char</code></samp>&rsquo;.
+See doc of <code>pg-subterm-start-char</code>.
 </p></dd></dl>
 <dl>
 <dt><a class="anchor" id="index-pg_002dtopterm_002dregexp"></a><u>Variable:</u> <b>pg-topterm-regexp</b></dt>
@@ -75,7 +75,7 @@ <h1 class="chapter">5. Goals Buffer Settings</h1>
 for example.  It could also be a literal command to insert and
 send back to the prover.
 </p>
-<p>The function &lsquo;<samp><code>pg-topterm-goalhyplit-fn</code></samp>&rsquo; examines text following this
+<p>The function <code>pg-topterm-goalhyplit-fn</code> examines text following this
 special character, to determine what kind of top element it is.
 </p>
 <p>This setting is also used to see if proof-by-pointing features
@@ -85,7 +85,7 @@ <h1 class="chapter">5. Goals Buffer Settings</h1>
 <dl>
 <dt><a class="anchor" id="index-pg_002dsubterm_002dend_002dchar"></a><u>Variable:</u> <b>pg-subterm-end-char</b></dt>
 <dd><p>Closing special character for subterm markup.<br>
-See &lsquo;<samp><code>pg-subterm-start-char</code></samp>&rsquo;.
+See <code>pg-subterm-start-char</code>.
 </p></dd></dl>
 
 
@@ -102,7 +102,7 @@ <h1 class="chapter">5. Goals Buffer Settings</h1>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>January 13, 2026</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>January 24, 2026</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>