		Search-engine friendly clone of the ACL2 documentation.

Xdoc

Constructors

Utilities to construct well-formed XDOC strings.

XDOC strings use XML tags, which must be properly matched and nested. They also use preprocessor directives, which can be regarded as ``tag''-like constructs that must also be properly matched and nested.

Starting with stringp values as the basic building blocks, the XDOC constructors provided here build trees that correspond to the combined structure of XML tags and preprocessor directives; these trees are recognized by the predicate treep. These trees also accommodate attributes of XML tags, whose values are subtrees, recursively. The function topstring turns these trees into strings, by recursively turning subtrees into strings, joining those strings, and adding XML tags and preprocessor directives at the roots of the trees.

With these XDOC constructors, one can write

(xdoc::topstring
   (xdoc::p "A paragraph.")
   (xdoc::ul
     (xdoc::li "One.")
     (xdoc::li "Two.")
     (xdoc::li "Three."))
   (xdoc::p "Another paragraph.")
   (xdoc::p "See "
            (xdoc::a :href "https://www.wikipedia.org" "Wikipedia")
            "."))

instead of

"<p>A paragraph.</p>
 <ul>
   <li>One.</li>
   <li>Two.</li>
   <li>Three.</li>
 </ul>
 <p>Another paragraph.</p>
 <p>See <a href="https://www.wikipedia.org">Wikipedia</a>.</p>"

The main advantage is that the XML tags (and preprocessor directives) will be always properly matched and nested by construction. Furthermore, using XDOC constructors is probably more readable, facilitates the modular and hierarchical construction of XDOC strings (in particular, see the composite XDOC constructors), and allows the insertion of comments within the XDOC constructor forms (e.g. lines of semicolons to visually separate sections).

The strings at the leaves of a tree may well contain XML tags or preprocessor directives. For relatively short XML-tagged text or preprocessor directives, it may be better to use tags and directives within a string rather than the corresponding XDOC constructors, e.g.

(xdoc::p "This is in <i>italics</i>.")

rather than

(xdoc::p "This is in " (xdoc::i "italics") ".")

In other words, it is not necessary to use XDOC constructors for everything, but only where they are convenient.

The books included by these XDOC constructor utilities should be minimized, to keep these utilities lightweight and more widely usable.

Subtopics

Primitive-constructors: Primitive XDOC constructors.
Composite-constructors: Composite XDOC constructors.
Constructor-preliminaries: Some preliminary utilities used by the XDOC constructors.
Trees: XDOC trees.