:doc or :more's ``(type :more...)''
Major Section: DOCUMENTATION
NOTE: The command :more only makes sense at the terminal.
Example: ACL2 !>:morewill continue printing whatever documentation was started by
:doc
or :more-doc.
When you type :doc name, for some documented name, the system
responds by typing the one-liner and the notes sections of the
documentation for 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.
Eventually :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. N and k
here are the values of the two state global variables
'more-doc-min-lines and 'more-doc-max-lines. You may use @ and
assign to inspect and set these variables, e.g.,
(@ more-doc-max-lines) will return the current maximum number of
lines printed by :more and (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 :more! instead.
