your response to :doc or :more's ``(type :more...)''

NOTE: The command :more only makes sense at the terminal.

ACL2 !>:more
will 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 !>:more
the 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.