*TERMINAL-MARKUP-TABLE*

a markup table used for printing to the terminal 
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 flag . fmt-string)
where key is one of the doc-string tilde directives (see markup), flag is a Boolean as described below, 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 an association list, binding keys based on arg as follows. 
#\p -- the `pointer'     ; only used if flag is t
#\s -- the print name version of the pointer, e.g., |abc| or ABC
#\c -- the parent file   ; only used if flag is t
#\t -- the displayed text
#\T -- uppercased displayed text
The first three entries are used only when the flag associated with key is t, indicating that the argument arg of ~key is to be parsed as starting with a symbol; for example, ~key[foo bar] will bind #\p to the symbol FOO.

The discussion of the above association list for printing fmt-string applies when printing documentation to other than the terminal as well. Such tools exist for Texinfo and for HTML; see files doc/write-acl2-html.lisp and doc/write-acl2-texinfo.lisp distributed with ACL2.