Auto-Update {userman, adaptingman}

href: ProofGeneral/PG@a78543c

Author: proofbot

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

@@ -168,7 +168,7 @@ <h2 class="section">14.3 Configuration variable mechanisms</h2>
 automatically be prefixed by the current proof assistant symbol.
 </p>
 <dl>
-<dt><a class="anchor" id="index-defpgcustom"></a><u>Macro:</u> <b>defpgcustom</b></dt>
+<dt><a class="anchor" id="index-defpgcustom"></a><u>Macro:</u> <b>defpgcustom</b><i> sym &amp;rest args</i></dt>
 <dd><p>Define a new customization variable &lt;PA&gt;<var>-sym</var> for the current proof assistant.<br>
 This is intended for defining settings which are useful for any prover,
 but which the user may require different values of across provers.
@@ -185,12 +185,12 @@ <h2 class="section">14.3 Configuration variable mechanisms</h2>
 can be used to give a default value for a generic setting.
 </p>
 <dl>
-<dt><a class="anchor" id="index-defpgdefault-1"></a><u>Macro:</u> <b>defpgdefault</b></dt>
+<dt><a class="anchor" id="index-defpgdefault-1"></a><u>Macro:</u> <b>defpgdefault</b><i> sym value</i></dt>
 <dd><p>Set default for the proof assistant specific variable &lt;PA&gt;<var>-sym</var> to <var>value</var>.<br>
 This should be used in prover-specific code to alter the default values
 for prover specific settings.
 </p>
-<p>Usage: (defpgdefault SYM <var>value</var>)
+<p>Usage: (defpgdefault <var>sym</var> <var>value</var>)
 </p></dd></dl>
 
 <p>All new instantiation variables are best declared using the
@@ -204,18 +204,18 @@ <h2 class="section">14.3 Configuration variable mechanisms</h2>
 macros are useful.
 </p>
 <dl>
-<dt><a class="anchor" id="index-proof_002dass"></a><u>Macro:</u> <b>proof-ass</b></dt>
-<dd><p>Return the value for SYM for the current prover.<br>
+<dt><a class="anchor" id="index-proof_002dass"></a><u>Macro:</u> <b>proof-ass</b><i> sym</i></dt>
+<dd><p>Return the value for <var>sym</var> for the current prover.<br>
 This macro should only be invoked once a specific prover is engaged.
 </p></dd></dl>
 <dl>
-<dt><a class="anchor" id="index-proof_002dass_002dsym"></a><u>Macro:</u> <b>proof-ass-sym</b></dt>
-<dd><p>Return the symbol for SYM for the current prover.  SYM not evaluated.<br>
+<dt><a class="anchor" id="index-proof_002dass_002dsym"></a><u>Macro:</u> <b>proof-ass-sym</b><i> sym</i></dt>
+<dd><p>Return the symbol for <var>sym</var> for the current prover.  <var>sym</var> not evaluated.<br>
 This macro should only be called once a specific prover is known.
 </p></dd></dl>
 <dl>
-<dt><a class="anchor" id="index-proof_002dass_002dsymv"></a><u>Macro:</u> <b>proof-ass-symv</b></dt>
-<dd><p>Return the symbol for SYM for the current prover.  SYM evaluated.<br>
+<dt><a class="anchor" id="index-proof_002dass_002dsymv"></a><u>Macro:</u> <b>proof-ass-symv</b><i> sym</i></dt>
+<dd><p>Return the symbol for <var>sym</var> for the current prover.  <var>sym</var> evaluated.<br>
 This macro should only be invoked once a specific prover is engaged.
 </p></dd></dl>
 
@@ -262,8 +262,8 @@ <h2 class="section">14.3 Configuration variable mechanisms</h2>
 </p></dd></dl>
 
 <dl>
-<dt><a class="anchor" id="index-proof_002ddeftoggle"></a><u>Macro:</u> <b>proof-deftoggle</b></dt>
-<dd><p>Define a function VAR-toggle for toggling a boolean customize setting VAR.<br>
+<dt><a class="anchor" id="index-proof_002ddeftoggle"></a><u>Macro:</u> <b>proof-deftoggle</b><i> var &amp;optional othername</i></dt>
+<dd><p>Define a function VAR-toggle for toggling a boolean customize setting <var>var</var>.<br>
 The toggle function uses &lsquo;<samp><code>customize-set-variable</code></samp>&rsquo; to change the variable.
 <var>othername</var> gives an alternative name than the default &lt;VAR&gt;-toggle.
 The name of the defined function is returned.

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

@@ -50,12 +50,12 @@ <h2 class="section">13.1 Default values for generic settings</h2>
 you should use the special <code>defpgdefault</code> macro:
 </p>
 <dl>
-<dt><a class="anchor" id="index-defpgdefault"></a><u>Macro:</u> <b>defpgdefault</b></dt>
+<dt><a class="anchor" id="index-defpgdefault"></a><u>Macro:</u> <b>defpgdefault</b><i> sym value</i></dt>
 <dd><p>Set default for the proof assistant specific variable &lt;PA&gt;<var>-sym</var> to <var>value</var>.<br>
 This should be used in prover-specific code to alter the default values
 for prover specific settings.
 </p>
-<p>Usage: (defpgdefault SYM <var>value</var>)
+<p>Usage: (defpgdefault <var>sym</var> <var>value</var>)
 </p></dd></dl>
 
 <p>In your prover-specific code you can simply use the setting
@@ -151,11 +151,11 @@ <h2 class="section">13.4 Useful functions and macros</h2>
 </p></dd></dl>
 
 <dl>
-<dt><a class="anchor" id="index-proof_002ddefshortcut"></a><u>Macro:</u> <b>proof-defshortcut</b></dt>
-<dd><p>Define shortcut function FN to insert <var>string</var>, optional keydef KEY.<br>
+<dt><a class="anchor" id="index-proof_002ddefshortcut"></a><u>Macro:</u> <b>proof-defshortcut</b><i> fn string &amp;optional key</i></dt>
+<dd><p>Define shortcut function <var>fn</var> to insert <var>string</var>, optional keydef <var>key</var>.<br>
 This is intended for defining proof assistant specific functions.
 <var>string</var> is inserted using &lsquo;<samp><code>proof-insert</code></samp>&rsquo;, which see.
-KEY is added onto proof assistant map.
+<var>key</var> is added onto proof assistant map.
 </p></dd></dl>
 <p>The function <code>proof-shell-invisible-command</code> is a useful utility
 for sending a single command to the process.  You should use this to
@@ -190,23 +190,23 @@ <h2 class="section">13.4 Useful functions and macros</h2>
 which invoke <code>proof-shell-invisible-command</code>.
 </p>
 <dl>
-<dt><a class="anchor" id="index-proof_002ddefinvisible"></a><u>Macro:</u> <b>proof-definvisible</b></dt>
-<dd><p>Define function FN to send <var>string</var> to proof assistant, optional keydef KEY.<br>
+<dt><a class="anchor" id="index-proof_002ddefinvisible"></a><u>Macro:</u> <b>proof-definvisible</b><i> fn string &amp;optional key</i></dt>
+<dd><p>Define function <var>fn</var> to send <var>string</var> to proof assistant, optional keydef <var>key</var>.<br>
 This is intended for defining proof assistant specific functions.
 <var>string</var> is sent using &lsquo;<samp><code>proof-shell-invisible-command</code></samp>&rsquo;, which see.
 <var>string</var> may be a string or a function which returns a string.
-KEY is added onto proof assistant map.
+<var>key</var> is added onto proof assistant map.
 </p></dd></dl>
 
 <dl>
-<dt><a class="anchor" id="index-proof_002ddefine_002dassistant_002dcommand"></a><u>Macro:</u> <b>proof-define-assistant-command</b></dt>
-<dd><p>Define FN (docstring DOC): check if <var>cmdvar</var> is set, then send <var>body</var> to prover.<br>
+<dt><a class="anchor" id="index-proof_002ddefine_002dassistant_002dcommand"></a><u>Macro:</u> <b>proof-define-assistant-command</b><i> fn doc cmdvar &amp;optional body</i></dt>
+<dd><p>Define <var>fn</var> (docstring <var>doc</var>): check if <var>cmdvar</var> is set, then send <var>body</var> to prover.<br>
 <var>body</var> defaults to <var>cmdvar</var>, a variable.
 </p></dd></dl>
 
 <dl>
-<dt><a class="anchor" id="index-proof_002ddefine_002dassistant_002dcommand_002dwitharg"></a><u>Macro:</u> <b>proof-define-assistant-command-witharg</b></dt>
-<dd><p>Define FN (arg) with DOC: check <var>cmdvar</var> is set, <var>prompt</var> a string and eval <var>body</var>.<br>
+<dt><a class="anchor" id="index-proof_002ddefine_002dassistant_002dcommand_002dwitharg"></a><u>Macro:</u> <b>proof-define-assistant-command-witharg</b><i> fn doc cmdvar prompt &amp;rest body</i></dt>
+<dd><p>Define <var>fn</var> (arg) with <var>doc</var>: check <var>cmdvar</var> is set, <var>prompt</var> a string and eval <var>body</var>.<br>
 The <var>body</var> can contain occurrences of arg.
 <var>cmdvar</var> is a variable holding a function or string.  Automatically has history.
 </p></dd></dl>

doc/master/userman/Concept-Index.html

@@ -180,8 +180,8 @@ <h1 class="unnumbered">Concept Index</h1>
 <tr><td></td><td valign="top"><a href="/doc/master/userman/Basic-Script-Management#index-proof-script-mode">proof script mode</a></td><td valign="top"><a href="/doc/master/userman/Basic-Script-Management#Script-buffers">2.3 Script buffers</a></td></tr>
 <tr><td></td><td valign="top"><a href="/doc/master/userman/Advanced-Script-Management-and-Editing#index-Proof-status-statistic">Proof status statistic</a></td><td valign="top"><a href="/doc/master/userman/Advanced-Script-Management-and-Editing#Proof-status-statistic">3.8 Proof status statistic</a></td></tr>
 <tr><td></td><td valign="top"><a href="/doc/master/userman/Coq-Proof-General#index-Proof-using">Proof using</a></td><td valign="top"><a href="/doc/master/userman/Coq-Proof-General#Proof-using-annotations">10.3 Proof using annotations</a></td></tr>
-<tr><td></td><td valign="top"><a href="/doc/master/userman/Coq-Proof-General#index-Proof_002dTree-visualization">Proof-Tree visualization</a></td><td valign="top"><a href="/doc/master/userman/Coq-Proof-General#Proof_002dTree-Visualization">10.11 Proof-Tree Visualization</a></td></tr>
 <tr><td></td><td valign="top"><a href="/doc/master/userman/Graphical-Proof_002dTree-Visualization#index-proof_002dtree-visualization">proof-tree visualization</a></td><td valign="top"><a href="/doc/master/userman/Graphical-Proof_002dTree-Visualization#Graphical-Proof_002dTree-Visualization">7. Graphical Proof-Tree Visualization</a></td></tr>
+<tr><td></td><td valign="top"><a href="/doc/master/userman/Coq-Proof-General#index-Proof_002dTree-visualization">Proof-Tree visualization</a></td><td valign="top"><a href="/doc/master/userman/Coq-Proof-General#Proof_002dTree-Visualization">10.11 Proof-Tree Visualization</a></td></tr>
 <tr><td colspan="3"> <hr></td></tr>
 <tr><th><a class="anchor" id="Concept-Index-1_cp_letter-Q">Q</a></th><td></td><td></td></tr>
 <tr><td></td><td valign="top"><a href="/doc/master/userman/Customizing-Proof-General#index-Query-program-name">Query program name</a></td><td valign="top"><a href="/doc/master/userman/Customizing-Proof-General#User-options">8.4 User options</a></td></tr>