a markup table used for printing to the terminal

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.