Major Section: DOCUMENTATION
The value of the ACL2 constant *terminal-markup-table* is an association
list pairing markup keys with strings, to be used for printing to the
terminal. See markup for a description of the ACL2 markup language.
The entries in *terminal-markup-table* are of the form
(key . fmt-string)where
key is one of the doc-string tilde directives
(see markup), and fmt-string is a string as expected by the
ACL2 printing function fmt. The system arranges that for any
arg, when an expression ~key[arg] is encountered by the
documentation printer, fmt will print fmt-string in the
association list where #\a is bound to arg and #\A is
bound to the result of applying the function string-upcase to
arg.
It is possible to implement tools in ACL2 for printing documentation
to other than the terminal. In fact, such tools exist for Texinfo
and for HTML. For now, discussion of this capability is beyond the
scope of the present topic.