1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
|
<html>
<head><title>MORE.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>MORE</h2>your response to <code>:</code><code><a href="DOC.html">doc</a></code> or <code>:</code><code><a href="MORE.html">more</a></code>'s ``<code>(type :more...)</code>''
<pre>Major Section: <a href="DOCUMENTATION.html">DOCUMENTATION</a>
</pre><p>
NOTE: The command <code>:more</code> only makes sense at the terminal.
<pre>
Example:
ACL2 !>:more
</pre>
will continue printing whatever <a href="DOCUMENTATION.html">documentation</a> was started by <code>:</code><code><a href="DOC.html">doc</a></code>
or <code>:</code><code><a href="MORE-DOC.html">more-doc</a></code>.
<p>
When you type <code>:doc name</code>, for some documented <code>name</code>, the system
responds by typing the one-liner and the notes sections of the
<a href="DOCUMENTATION.html">documentation</a> for <code>name</code>. It then types
``<code>(type :more for more, :more! for the rest)</code>''. If you then type
<pre>
ACL2 !>:more
</pre>
the system will start to print the details section of <code>name</code>. The
same thing could be achieved by typing <code>:more-doc name</code>, but that
requires you to type name again.<p>
Similarly, if you have typed <code>:</code><code><a href="MORE-DOC.html">more-doc</a></code> name, the system will print
the first ``block'' of the details section and then print
``<code>(type :more for more, :more! for the rest)</code>''. Typing <code>:more</code> at that
point will cause the next block of the details section to be printed.
Eventually <code>:more</code> will conclude by printing ``<code>*-</code>'' which is the
indicator that the text has been exhausted.<p>
What is a ``block'' of text? <code>:More</code> looks for the end of a paragraph
(two adjacent newlines) after printing <code>n</code> lines. If it doesn't find
one before it has printed <code>k</code> lines, it just stops there. <code>N</code> and <code>k</code>
here are the values of the two <a href="STATE.html">state</a> global variables
<code>'more-doc-min-lines</code> and <code>'more-doc-max-lines</code>. You may use <code><a href="_at_.html">@</a></code> and
<code><a href="ASSIGN.html">assign</a></code> to inspect and set these variables, e.g.,
<code>(@ more-doc-max-lines)</code> will return the current maximum number of
lines printed by <code>:more</code> and <code>(assign more-doc-max-lines 19)</code> will
set it to 19. On terminals having only 24 lines, we find min and
max settings of 12 and 19 the most pleasant.<p>
If you want <code>:more</code> to print all of the details instead of feeding
them to you one block at a time, type <code>:</code><code><a href="MORE_bang_.html">more!</a></code> instead.
<br><br><br><a href="acl2-doc.html"><img src="llogo.gif"></a> <a href="acl2-doc-index.html"><img src="index.gif"></a>
</body>
</html>
|
