		Search-engine friendly clone of the ACL2 documentation.

Xdoc

Terminal

Display of XDOC tags at the terminal or in ACL2::ACL2-doc

For relevant background see markup. This topic discusses the display of certain XDOC tags when using either the :doc command at the terminal or the ACL2::ACL2-doc browser for Emacs. We begin with a brief summary that should suffice for most users, followed by basic information about three ways to display marked-up text, and concluding with design notes followed by further information including additional options provided by building text-based manuals.

Summary

The following tags, which we call “font tags”, indicate a desired font; see markup.

bold
italics
emphasis
underline
<tt>typewriter text</tt>

Note that the XDOC preprocessor replaces @('{some text}') with <v>{some text}</v>, which is treated as described here for <tt>{some text}</tt>.

By default, the :doc command at the terminal and the ACL2-Doc browser attempt to handle font tags as indicated above. (There can be variations depending on your platform; for example, sometimes text to be italicized is displayed with underlining.) The next section discusses ways to modify that that behavior without having to rebuild the manuals; then we discuss rebuilding the manuals.

Three ways to display marked-up text

The behaviors of the font tags correspond to the legal values of environment variable "ACL2_XDOC_TAGS", as follows.

"FANCY", "", or (the default) nil, representing what is refernced below as a “fancy environment”:
An attempt is made to use a font that conveys the intention, as follows.
- ..: bold text, often red or blue to help it to stand out
- ..: italics
- ..: italics
- ..: underlined
- <tt>..</tt>: grey background
"SIMPLE":
The font tags are handled as follows.
- ..: Replace each of and by two underscores, __.
- ..: Replace each of and by an underscore, _.
- ..: Replace each of and by an underscore, _.
- ..: Replace each of and by an underscore, _.
- <tt>..</tt>: Just drop <tt> and </tt>
"PLAIN":
The font tags are all dropped; that is, the text is printed as though the tags were not present.

As noted above, the default is a fancy environment, where the :doc command and ACL2-Doc browser attempt to handle font tags as indicated (italic, etc.). Technically, this is controlled by the addition of so-called Select Graphic Rendition (SGR) control sequences when rendering the documentation as text. Customization of this behavior depends on the following three cases.

For the built-in :doc command this behavior cannot be customized.
However, behavior is fully customizable for the “modified :doc” command, which is the :doc command provided by xdoc, for example after evaluating (include-book "xdoc/init" :dir :system). One simply sets environment variable "ACL2_XDOC_TAGS" according to the desired case of the three cases above. This can be done either before starting ACL2 or else by calling setenv$ inside ACL2, e.g., (setenv$ "ACL2_XDOC_TAGS" "PLAIN").
For ACL2-Doc the behavior is partially customizable. For a default build of the manual (which however can be overridden as described in the next section), one cannot get the behavior described above for "SIMPLE". However, if you set environment variable "ACL2_XDOC_TAGS" to "PLAIN" or "SIMPLE" in a way that is visible to Emacs, you can eliminate the SGR control sequences so that you see plain text. One way to accomplish this is to evaluate the form (setenv "ACL2_XDOC_TAGS" "PLAIN") inside Emacs.

Design notes

Here we make a few observations about why font tags are handled as they are.

We have seen that for a fancy environment, text within ... is rendered not only as bold but also as red. That is because bold text does not often show up clearly.
The use of ‘*’ as a delimiter is avoided because that character so often appears in ACL2 names, in particular, in constant symbols. Underscore, by contrast, appears much less often.
The use of a grey background (which may technically be called “white”, but it's really grey!) is rather common for fixed-width code text, so it seems a good choice for the <tt> tag in a fancy environment.

Changing the default builds of text-based manuals

The remainder of this topic can probably be ignored by most. It discusses how to build the text-based documentation used by :doc and ACL2-Doc to modify handling of the font tags above.

First let us review basics of how :doc, modified :doc, and ACL2-Doc work. These all read a text-based manual that has been built by removing all preprocessor directives and all tags, including font tags. By default, these are built in a fancy environment (as defined above), which inserts SGR control sequences for font tags. Terminals often intepret these tags by displaying text using suitable fonts (italics, underline, etc.), and this is how text is displayed by :doc. ACL2-Doc invokes Emacs utilities to provide such fonts. We are ready to explain the restrictions above.

The built-in :doc command simply prints out the rendered text, which is why its behavior cannot be customized (unless perhaps one modifies the terminal environment).
If Emacs sees a value of environment variable "ACL2_XDOC_TAGS" of "PLAIN" or "SIMPLE", it removes SGR control sequences from the rendered text before displaying it as plain text. But there is no way to take that rendered text and add markings as specified for the "SIMPLE" case.

On the other hand, the modified :doc command renders the original documentation, which still has tags. That rendering is sensitive to the value of environment variable "ACL2_XDOC_TAGS". But the items above tells us that there is not the same flexibility for the built-in :doc command or ACL2-Doc.

The only way to get such flexibility is to build text-based manuals for :doc and ACL2-Doc that render text as desired, which requires setting environment variable "ACL2_XDOC_TAGS" when building thse manuals. Since :doc is based off ACL2 source file doc.lisp, which is to be modified only by the ACL2 implementors, we focus on building the documentation for ACL2-Doc.

The ACL2+books rendered manual is file books/system/doc/rendered-doc-combined.lsp, and there is also an “ACL2 only” manual restricted to built-in functions in file books/system/doc/rendered-doc.lsp. These can be built with any of the three default behaviors (fancy, simple, or plain) by setting the environment variable "ACL2_XDOC_TAGS" before building those manuals, for example as follows while standing in the books directory. The --acl2 and -j options are up to the user. Note: You might need first to delete file doc/top.cert under books/.

(export ACL2_XDOC_TAGS=FANCY ; ./build/cert.pl --acl2 acl2 doc/top)
(export ACL2_XDOC_TAGS=SIMPLE ; ./build/cert.pl --acl2 acl2 doc/top)
(export ACL2_XDOC_TAGS=PLAIN ; ./build/cert.pl --acl2 acl2 doc/top)

For example, suppose you want underscores to surround text that is marked with , so that for example “italicized text” is printed as “_italicized text_”. It then suffices to build the manual with "SIMPLE" as in the second command displayed above, except that when using :doc at the terminal you would first need to include the ACL2::community-book "xdoc/init" as discussed above, so that you are using the modified :doc command.

We close by describing an implementation detail; ideally it can be ignored, but we mention it in case someone finds it to be useful. When the manual is built (by certifying ACL2::community-book doc/top), a file is created, system/doc/acl2-doc-search, that is consulted by search commands in ACL2-Doc. When that file is built in a fancy environment (which, again, is the default), then environment variable ACL2_XDOC_TAGS is first temporarily bound to "PLAIN" so that system/doc/acl2-doc-search will not contain any SGR control sequences that might cause search mismatches.