Auto-Update {userman, adaptingman}

href: ProofGeneral/PG@b82c219

Author: proofbot

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/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></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 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>

doc/master/userman/Customizing-Proof-General.html

@@ -289,20 +289,20 @@ <h2 class="section">8.3 Display customization</h2>
 </p><table><tr><td>&nbsp;</td><td><pre class="lisp">  where the three useful buffers are displayed: scripting
   buffer, goals buffer and response buffer.
 
-  Here are the three modes:
+  The three possible modes are:
 
   - vertical: the 3 buffers are displayed in one column.
   - hybrid: 2 columns mode, left column displays scripting buffer
     and right column displays the 2 others.
   - horizontal: 3 columns mode, one for each buffer (script, goals,
     response).
 
-  By default, the display mode is automatically chosen by
-  considering the current Emacs frame width: if it is smaller
-  than &lsquo;<samp><code>split-width-threshold</code></samp>&rsquo; then vertical mode is chosen,
-  otherwise if it is smaller than 1.5 * &lsquo;<samp><code>split-width-threshold</code></samp>&rsquo;
-  then hybrid mode is chosen, finally if the frame is larger than
-  1.5 * &lsquo;<samp><code>split-width-threshold</code></samp>&rsquo; then the horizontal mode is chosen.
+  By default, the display mode is <code>'smart</code> which automatically choses
+  between these 3 modes by considering the current Emacs frame width: if
+  it is smaller than &lsquo;<samp><code>split-width-threshold</code></samp>&rsquo; then vertical mode is
+  chosen, otherwise if it is smaller than 1.5 * &lsquo;<samp><code>split-width-threshold</code></samp>&rsquo;
+  then hybrid mode is chosen, finally if the frame is larger than 1.5 *
+  &lsquo;<samp><code>split-width-threshold</code></samp>&rsquo; then the horizontal mode is chosen.
 
   You can change the value of &lsquo;<samp><code>split-width-threshold</code></samp>&rsquo; at your
   will.