		Search-engine friendly clone of the ACL2 documentation.

Xdoc

Markup

The XML markup language that is the basis of XDOC documentation strings.

XDOC uses an XML markup language that is similar to a subset of HTML. Note that unlike HTML, beginning and ending tags are case-sensitive and must match exactly. As in HTML, you must escape characters like < in text to distinguish them from tags.

Formatting Text

Various tags allow you to control the font:

<b>bold</b>
<i>italics</i>
<u>underline</u>
<tt>typewriter text</tt>
<color rgb="#ff0000">colored text</color>
<sf>sans-serif</sf>

See terminal for how such tags are displayed at the terminal or with the ACL2::ACL2-doc browser for Emacs.

Displaying Source Code

The preprocessor allows you to insert function definitions, theorems, etc., from the ACL2 world. This can help you avoid having to copy and paste definitions into your documentation, which can help to keep your documentation up to date.

But sometimes you want to write other kinds of code fragments as examples. The raw markup options are:

Use the <tt> tag for short, inline pieces of code, such as (+ 1 x).
Use the <code> tag for longer code examples that should be indented and "preformatted," i.e., newlines and spaces should be preserved.

However, it's often better to use the preprocessor's @('...') and @({...}) macros, respectively. These are nice because they automatically escape special HTML characters like < into < and also automatically add hyperlinks to documented functions.

(Implementation Note. The <tt> and <code> tags in XDOC do not correspond to the <tt> and <code> tags in HTML. In fact, <tt> is rendered with an HTML <span>, and <code> is rendered with an HTML <pre>.)

Whenever you include Lisp code fragments in your documentation, you should usually keep everything indented one space to prevent Emacs problems. For instance:

|(defxdoc foo
|  :long "<h3>How to format @('<code>') blocks</h3>
|
|<p>GOOD -- the form is indented one space:</p>
|<code>
| (my-lisp-form (foo ...)
|               (bar ...))
|</code>
|
|<p>BAD -- the form is directly on the left-margin:</p>
|<code>
|(my-lisp-form (foo ...)
|              (bar ...))
|</code>

Without this leading space, Emacs can become confused and think that (my-lisp-form ...), rather than (defxdoc foo ...), is the top-level expression. This can ruin syntax highlighting and also commands like C-t e for sending s-expressions to the *shell* window.

Hyperlinks

Internal links between documentation topics and Emacs tags-search links into the source code are handled by the preprocessor.

You can add external links to web pages with ordinary HTML-style links, e.g.,

<a href="https://www.cs.utexas.edu/">University of Texas Department of
Computer Science</a>

produces a link to the University of Texas Department of Computer Science.

Typesetting Mathematics (Experimental)

XDOC's fancy web viewer now has some support for LaTeX-like mathematics. For instance, you can write formulas such as

c = \pm\sqrt{b^2 + a^2}

See katex-integration for details.

Images and other Resources

Documentation topics can include inline images and (via hyperlinks) can refer to other kinds of files, like PDF files. You have to tell XDOC where to find these files; see add-resource-directory. After setting up a suitable resource directory, you can use img tags such as:

<img src='res/centaur/centaur-logo.png'/>

to produce output such as:

Structuring Documents

<h1> creates the biggest heading

<h2> the next biggest

<h3> a medium size heading (a good default)

<h4> a smaller heading

<h5> a very small heading

<p> tags should be put around paragraphs.

<blockquote> can be used to create indented paragraphs like this one. (Let's put enough text here to make it word-wrap. Mumble mumble mumble. Mumble. Mumble mumble.)

<br/> can be used
to write haikus and so on
but is discouraged

Bulleted and numbered lists work as in HTML. The list itself begins with <ul> (for bulleted lists) or <ol> (for numbered lists). Each list element is an <li> tag. For instance,

<ul>
  <li>one</li>
  <li>two</li>
  <li>three</li>
</ul>

Produces:

one
two
three

You can also use definition lists, which are comprised of <dl>, <dt>, and <dd> tags. For instance,

<dl>
  <dt>Inputs</dt>
  <dd><tt>x</tt>, the list we are traversing</dd>
  <dd><tt>max</tt>, limit on how many we can accumulate</dd>
  <dd><tt>acc</tt>, accumulator for our results</dd>
</dl>

Produces:

Inputs: x, the list we are traversing; max, limit on how many we can accumulate; acc, accumulator for our results

These framed boxes are generated with the <box> tag.

A subset of HTML tables is implemented, including <table>, <tr>, <th>, and <td>. To encourage portability, this is a somewhat limited facility—you cannot control widths, padding, etc. on table cells. Here is an example table:

Color	Land	Power Source
White	Plains	Goodness, order and light, all that is richeous and holy. Adversary of evil and chaos.
Blue	Islands	Air and water, knowledge and control, illusion and sleight of hand. Adversary of chaos and nature.
Black	Swamps	Evil, darkness and despair, ambition and will, suffering and death. Adversary of nature and goodness.
Red	Mountains	Fire and chaos, impulsiveness and fury, freedom and whimsy. Adversary of goodness and control.
Green	Forests	Life and nature, growth and fertility. Adversary of control and death.

It's relatively easy to add new tags. There is undocumented support for images and icons, but this is currently awkward. In the future, we may add other tags that users request.