Major Section: DOCUMENTATION
NOTE: The command
:more only makes sense at the terminal.
Example: ACL2 !>:morewill continue printing whatever documentation was started by
When you type
:doc name, for some documented
name, the system
responds by typing the one-liner and the notes sections of the
name. It then types
(type :more for more, :more! for the rest)''. If you then type
ACL2 !>:morethe system will start to print the details section of
name. The same thing could be achieved by typing
:more-doc name, but that requires you to type name again.
Similarly, if you have typed
more-doc name, the system will print
the first ``block'' of the details section and then print
(type :more for more, :more! for the rest)''. Typing
:more at that
point will cause the next block of the details section to be printed.
:more will conclude by printing ``
*-'' which is the
indicator that the text has been exhausted.
What is a ``block'' of text?
:More looks for the end of a paragraph
(two adjacent newlines) after printing
n lines. If it doesn't find
one before it has printed
k lines, it just stops there.
here are the values of the two state global variables
'more-doc-max-lines. You may use
assign to inspect and set these variables, e.g.,
(@ more-doc-max-lines) will return the current maximum number of
lines printed by
(assign more-doc-max-lines 19) will
set it to 19. On terminals having only 24 lines, we find min and
max settings of 12 and 19 the most pleasant.
If you want
:more to print all of the details instead of feeding
them to you one block at a time, type