topics

(in-package "XDOC")

(include-book "top")

(defxdoc xdoc
  :parents (documentation)
  :short "<i>XDOC</i> is a tool for documenting ACL2 books.  You can use it to
access documentation about ACL2 and its books, to document your own books, and
to create custom web-based manuals."
  :long "<p>Below we cover how to use XDOC to build manuals or document your
own @(see acl2::books).  If you just want to browse the documentation, you
probably don't need to read any of this!  Instead, see @(see
documentation).</p>

<h3>Starting Points</h3>

<p>A good, tutorial-style introduction to XDOC can be found in:</p>

<blockquote>
Jared Davis and Matt Kaufmann.  <a
href='http://dx.doi.org/10.4204/EPTCS.152.2'>Industrial Strength Documentation
for ACL2</a>.  ACL2 Workshop 2014.  EPTCS 152.  Pages 9-25.
</blockquote>

<p>See <i>Building the Manual</i> under @(see acl2::books-certification) for
information on building the ACL2+Books manual.  See @(see testing) for easy
instructions for how to test your XDOC strings.</p>


<p>To use XDOC to document your own books, the first step is:</p>

@({
 (include-book "xdoc/top" :dir :system)
})

<p>This book loads very quickly and requires no ttags.  It gives you @(see
defxdoc) and @(see defsection), the basic commands for adding documentation.
It also installs a new @(':doc') command, via @(see ld-keyword-aliases), so
that you can see new documentation from the terminal.</p>

<p>For a possibly more convenient way to construct XDOC strings, do the
following:</p>

@({
 (include-book "xdoc/constructors" :dir :system)
})

<p>This book includes community book @('xdoc/top.lisp'), and in addition
provides utilities to construct well-formed XDOC strings in a modular way.  See
<see topic='@(url xdoc::constructors)'>the documentation</see> for more
details.</p>

<p>Once you have documented your books, you may wish to create a manual that
can be viewed from a web browser or from the @(see acl2::acl2-doc) Emacs-based
browser.  You can do this quite easily with XDOC's @(see save) command.
This command can be embedded in an ordinary ACL2 book, so that your manual is
automatically regenerated when you build your project.</p>


<h3>New Features</h3>

<p>XDOC now supports @(see katex-integration) for writing LaTeX-like formulas
like
@($
\left( \sum_{i=0}^{n} \sqrt{f(i)} \right) < \frac{n^2}{k}
$)
within your documentation.</p>

<p>When writing documentation, you can now optionally have XDOC topics
automatically displayed as you submit new @(see defxdoc) forms&mdash;just
add:</p>

@({
 (include-book "xdoc/debug" :dir :system)
})

<p>to your @(see acl2::acl2-customization) file, or include it while you are
developing your book.  Afterward, each @(see defxdoc) form you submit will be
immediately shown at the terminal, giving you a quick, text-mode preview that
may help you to diagnose any markup problems.</p>")

(defxdoc missing-parents-test
  :short "A topic with no @(':parents')."
  :long "<p>This topic has no @(':parents') and is just meant to ensure that
@(see missing-parents) is working correctly.</p>")

(local (set-default-parents xdoc))

(defxdoc defxdoc
  :short "Add documentation to the @(see xdoc) database."
  :long "<box><p>Note: @('defxdoc') is very basic.  You will usually want to
use @(see defsection) or @(see std::define) instead.</p></box>

<p>@('Defxdoc') is the XDOC alternative to ACL2's built-in @('defdoc')
command.</p>

<p>General form:</p>

@({
 (defxdoc name
   [:parents parents]
   [:short   short]
   [:long    long])
})

<p>Example:</p>

@({
 (defxdoc duplicity
   :parents (std/lists defsort count no-duplicatesp)
   :short "@(call duplicity) counts how many times the
            element @('a') occurs within the string @('x')."
   :long "<p>This function is similar to ACL2's built-in
          @('count') function but is more limited:</p>  ...")
})

<p>The @('name') of each documentation topic must be a symbol.  All of the
keyword arguments are optional:</p>

<ul>

<li>@('parents') let you associate this documentation with other topics.  A
topic may have many parents, but circular chains of parents are not allowed and
will lead to errors when generating manuals.  If no @(':parents') are given
explicitly, the <see topic='@(url set-default-parents)'>default parents</see>
will be used.</li>

<li>@('short') should be a short description of this topic that is suitable for
inlining in other pages.  For instance, it may be displayed in subtopic listing
and in "hover" text on navigation pages.</li>

<li>@('long') should be the full, detailed documentation for this topic.</li>

</ul>

<p>The @('short') and @('long') strings may be written using the XDOC @(see
markup) language, and may also use @(see preprocessor) commands to insert
function definitions, theorems, topic links, and so on.</p>

<p>Many examples of using XDOC can be found throughout the ACL2 books.  See for
instance the @(see acl2::std), @(see acl2::std/strings) or @(see
acl2::std/osets) libraries.</p>

<h3>Note for Advanced Users</h3>

<p>XDOC just stores its documentation in an ordinary ACL2 table, so if you want
to do something like automatically generate documentation from macros, you
might decide to bypass @('defxdoc') and just manipulate the table directly.</p>

<p>It is not possible to directly use @('defxdoc') from raw Lisp, but you can
use @(see defxdoc-raw) instead.</p>")

(defxdoc markup
  :short "The <a href='http://en.wikipedia.org/wiki/Xml'>XML</a> markup
language that is the basis of XDOC documentation strings."
  :long "<p>XDOC uses an XML markup language that is similar to a subset of <a
href='http://en.wikipedia.org/wiki/HTML'>HTML</a>.  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.</p>

<h3>Formatting Text</h3>

<p>Various tags allow you to control the font:</p>
<ul>
 <li><b>&lt;b&gt;bold&lt;/b&gt;</b></li>
 <li><i>&lt;i&gt;italics&lt;/i&gt;</i></li>
 <li><u>&lt;u&gt;underline&lt;/u&gt;</u></li>
 <li><tt>&lt;tt&gt;typewriter text&lt;/tt&gt;</tt></li>
 <li><color rgb="#ff0000">&lt;color rgb=&quot;#ff0000&quot;&gt;colored text&lt;/color&gt;</color></li>
 <li><sf>&lt;sf&gt;sans-serif&lt;/sf&gt;</sf></li>
</ul>

<p>See @(see terminal) for how such tags are displayed at the terminal or with
the @(see acl2::ACL2-Doc) browser for Emacs.</p>

<h3>Displaying Source Code</h3>

<p>The @(see 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.</p>

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

<ul>

<li>Use the @('<tt>') tag for short, inline pieces of code, such as <tt>(+ 1
x)</tt>.</li>

<li>Use the @('<code>') tag for longer code examples that should be indented
and "preformatted," i.e., newlines and spaces should be preserved.</li>

</ul>

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

<p>(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>').)</p>

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

@({
|(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>
})

<p>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.</p>




<h3>Hyperlinks</h3>

<p><i>Internal links</i> between documentation topics and <i>Emacs tags-search
links</i> into the source code are handled by the @(see preprocessor).</p>

<p>You can add <i>external links</i> to web pages with ordinary HTML-style
links, e.g.,</p>

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

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


<h3>Typesetting Mathematics (Experimental)</h3>

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

@([
     c = \pm\sqrt{b^2 + a^2}
])

<p>See @(see katex-integration) for details.</p>


<h3>Images and other Resources</h3>

<p>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 @(see add-resource-directory).  After setting up a
suitable resource directory, you can use @('img') tags such as:</p>

@({
    <img src='res/centaur/centaur-logo.png'/>
})

<p>to produce output such as:</p>

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


<h3>Structuring Documents</h3>

<h1>@('<h1>') creates the biggest heading</h1>
<h2>@('<h2>') the next biggest</h2>
<h3>@('<h3>') a medium size heading (a good default)</h3>
<h4>@('<h4>') a smaller heading</h4>
<h5>@('<h5>') a very small heading</h5>

<p>@('<p>') tags should be put around paragraphs.</p>

<blockquote>@('<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.)</blockquote>

<p>@('<br/>') can be used<br/>
to write haikus and so on<br/>
but is discouraged</p>

<p>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,</p>

@({
<ul>
  <li>one</li>
  <li>two</li>
  <li>three</li>
</ul>
})

<p>Produces:</p>

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

<p>You can also use definition lists, which are comprised of @('<dl>'),
@('<dt>'), and @('<dd>') tags.  For instance,</p>

@({
<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>
})

<p>Produces:</p>

<box>
<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>
</box>

<p>These framed boxes are generated with the @('<box>') tag.</p>

<p>A subset of HTML tables is implemented, including @('<table>'), @('<tr>'),
@('<th>'), and @('<td>').  To encourage portability, this is a somewhat limited
facility&mdash;you cannot control widths, padding, etc. on table cells. Here is
an example table:</p>

<table>
<tr> <th>Color</th> <th>Land</th>   <th>Power Source</th> </tr>

<tr> <td>White</td> <td>Plains</td>
     <td>Goodness, order and light, all that is richeous and holy.  Adversary
         of evil and chaos.</td>
</tr>

<tr> <td>Blue</td>  <td>Islands</td>
     <td>Air and water, knowledge and control, illusion and sleight of hand.
         Adversary of chaos and nature.</td>
</tr>

<tr> <td>Black</td>  <td>Swamps</td>
     <td>Evil, darkness and despair, ambition and will, suffering and death.
         Adversary of nature and goodness.</td>
</tr>

<tr> <td>Red</td>  <td>Mountains</td>
     <td>Fire and chaos, impulsiveness and fury, freedom and whimsy.
         Adversary of goodness and control.</td>
</tr>

<tr> <td>Green</td> <td>Forests</td>
     <td>Life and nature, growth and fertility.  Adversary of control and
         death.</td>
</tr>
</table>


<p>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.</p>")

(defpointer syntax markup)

(defxdoc preprocessor
  :short "In addition to its @(see markup) language, XDOC includes a
preprocessor which can be used to interpret certain directives of the form
@('@(...)')."
  :long "<h3>Functions and Theorems</h3>

<p>To look up function definitions (or pieces of definitions) from the ACL2
world and insert them into your documentation, you can use:</p>

<table>

<tr>  <td>@('@(def fn)')</td>
      <td>insert the definition of <i>fn</i><br/>
          (also works for theorems, macros, ...)</td>
</tr>

<tr>  <td>@('@(def? fn)')</td>
      <td>Same as @('@(def fn)') but doesn't
          produce an error if the definition isn't found</td>
</tr>

<tr> <td>@('@(body fn)')</td>
     <td>just the body of <i>fn</i></td> </tr>

<tr> <td>@('@(formals fn)')</td>
     <td>just the formals of <i>fn</i></td> </tr>

<tr> <td>@('@(measure fn)')</td>
     <td>just the measure of <i>fn</i></td> </tr>

<tr> <td>@('@(call fn)')</td>
     <td>a generic function call of <i>fn</i></td> </tr>

</table>

<p>We expect that @('def') and @('body') directives will expand to large code
fragments, so they are automatically wrapped in @('<code>') blocks.</p>

<p>The @('call') directive is automatically wrapped in @('<tt>') tags, i.e.,
@('@(call fib)') might become @('<tt>(fib x)</tt>').  An alternative is to use
@('@(ccall fib)'), for "code call," which inserts @('<code>') tags instead;
this could be more appropriate for functions with many arguments.</p>

<p>The other directives just become plain text, and you can wrap whatever
formatting commands you like around them and use them inline in paragraphs,
etc.</p>

<h3>Adding Examples or Code Fragments</h3>

<p>There is special syntax to put in raw or verbatim text.  This is especially
useful for examples and code fragments, where you don't want to have to escape
special character like @('<') with @('&lt;').</p>

<ul>
<li><tt>@@('...')</tt> inserts @('...') into @('<tt>') XDOC tags.</li>
<li><tt>@@({...})</tt> inserts @('...') into @('<code>') XDOC tags.</li>
</ul>

<p>These have a special feature for automatically linking to documented topics.
For instance, <tt>@@('(consp x)')</tt> produces @('(consp x)'), and
<tt>@@({ (consp x) })</tt> produces:</p>

@({
 (consp x)
})

<h3>Evaluating Lisp from Doc Strings</h3>

<p>The preprocessor has a special backtick syntax for dynamically evaluating
ACL2 expressions.  This can be used to inject constants and examples into your
documentation.  For instance:</p>

<ul>
<li>@('@(`(+ 1 2 3)`)')          produces @(`(+ 1 2 3)`)</li>
<li>@('@(`(mv 'a 10 state)`)')   produces @(`(mv 'a 10 state)`)</li>
<li>@('@(`acl2::*pkg-witness-name*`)') produces @(`acl2::*pkg-witness-name*`)</li>
</ul>

<p>By default, the backtick syntax introduces @('<tt>') tags and automatically
escapes any special XML characters like @('<').  Sometimes this isn't what you
want.  When the result of your evaluation is large, you can use a spcial
@(':code') prefix to insert @('<code>') tags instead.  For instance:
@('@(`(:code (make-list 100))`)') produces:</p>

@(`(:code (make-list 100))`)

<p>(Advanced) Introducing @('<tt>') tags also doesn't work well for certain,
sophisticated uses of evaluation, e.g., to generate hyperlinks, etc.  The
special @(':raw') prefix can be used to insert exactly the contents of a
string, with no automatic escaping.  For instance:
  @('  @(`(:raw "a &lt; b")`)  ') produces
       @(`(:raw "a &lt; b")`).
Note that it is quite easy to use @(':raw') incorrectly; you have to escape
things properly yourself!</p>

<h3>Emacs Links</h3>

<p>The @('@(srclink name)') directive inserts a source-code link for users who
have configured their web browser as described in @(see emacs-links).  For
documentation in the acl2-doc browser @(see acl2::acl2-doc) or at the terminal,
the name is enclosed in angle brackets (@('<name>')), which essentially
represent a source-code link when using the acl2-doc `@('/')' command.</p>

<p>It is often unnecessary to use @('srclink') directly, because these links
are automatically inserted by @('@(def fn)').  One good reason to use
@('srclink') is to link to macros like @(srclink defxdoc), which often are
written using backquote and hence do not display nicely.</p>

<p>Source links are sometimes inappropriate, e.g., for definitions or theorems
that are generated by macros.  You can suppress the automatic source links on
@('def') commands by using @('@(gdef fn)') instead.  This stands for
"generated definition."</p>


<h3>Documentation Links</h3>

<p>The easiest way to link between topics is to use @('@(see name)'), which
expands into a link to @('name').  The text shown to the reader is just the
name of the topic, typically in lower case though the case may be preserved,
for example if a topic name has mixed case.  Note also that @('@(csee name)')
can be used for links whose first letter should be capitalized; that @('@(tsee
name)') can be used for links that should appear in type-writer font; and that
@('@(see?  name)') is useful for macros, since a link is inserted if @('name')
is documented but otherwise @('name') simply appears in typewriter font.</p>

<p>For most purposes, @('@(see name)') is adequate and it is also recommended.
Finer-grained control (e.g., changing the link text) is also possible, but then
you have to understand how file names get mangled.  The basic story is that
@('@(see name)') expands to:</p>

@({
<see topic="mangled-topic-name">printed-topic-name</see>
})

<p>Where:</p>

<ul>

<li>@('mangled-topic-name') is a canonical, url/file-name friendly,
human-hostile mangling of @('name')'s package and symbol names, and</li>

<li>@('printed-topic-name') is an XML-escaped variant of @('name'), e.g., where
@('<') becomes @('&lt;'), etc.; depending on the package of the current topic's
name, it may or may not include the package portion of @('name').</li>

</ul>

<p>So, to support custom links, we provide</p>

<ul>
 <li>@('@(url name)'), which expands to @('mangled-topic-name')</li>
 <li>@('@(sym name)'), which expands to @('printed-topic-name')</li>
 <li>@('@(csym name)'), like @('sym'), but with the first letter capitalized</li>
</ul>

<p>You can use these to write your own @('<see>') tags.  You should probably
<i>never</i> write a @('<see>') tag yourself without using @('@(url ...)').
Some examples:</p>

<ul>
<li>@('@(url defxdoc)') expands to @(url defxdoc)</li>
<li>@('@(sym defxdoc)') expands to @(sym defxdoc)</li>
<li>@('@(csym defxdoc)') expands to @(csym defxdoc)</li>
</ul>

<h3>Escaping of @</h3>

<p>Since @('@(') is intercepted by the preprocessor, you may occasionally need
to escape it.  You can write @('@@') to generate a single @('@') sign.</p>

<p>Besides @('@(') and @('@@'), the preprocessor leaves any other uses of
@('@') intact.  So, most uses of @('@'), such as in email addresses, do not
need to be escaped.</p>")

(defxdoc terminal
  :short "Display of XDOC tags at the terminal or in @(see acl2::ACL2-Doc)"
  :long "<p>For relevant background see @(see markup).  This topic discusses
the display of certain XDOC tags when using either the @(':')@(see doc) command
at the terminal or the @(see 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.</p>

<h3>Summary</h3>

<p>The following tags, which we call &ldquo;font tags&rdquo;, indicate a
desired font; see @(see markup).</p>

<ul>
 <li><b>&lt;b&gt;bold&lt;/b&gt;</b></li>
 <li><i>&lt;i&gt;italics&lt;/i&gt;</i></li>
 <li><em>&lt;em&gt;emphasis&lt;/em&gt;</em></li>
 <li><u>&lt;u&gt;underline&lt;/u&gt;</u></li>
 <li><tt>&lt;tt&gt;typewriter text&lt;/tt&gt;</tt></li>
</ul>

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

<p>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.</p>

<h3>Three ways to display marked-up text</h3>

<p>The behaviors of the font tags correspond to the legal values of environment
variable @('"ACL2_XDOC_TAGS"'), as follows.</p>

<ul>

<li>@('"FANCY"'), @('""'), or (the default) @('nil'), representing what is
refernced below as a &ldquo;fancy environment&rdquo;:<br/>An attempt is made to
use a font that conveys the intention, as follows.

<ul>
 <li>@('<b>..</b>'): bold text, often red or blue to help it to stand out</li>
 <li>@('<i>..</i>'): italics</li>
 <li>@('<em>..</em>'): italics</li>
 <li>@('<u>..</u>'): underlined</li>
 <li>@('<tt>..</tt>'): grey background</li>
</ul>
</li>

<li>@('"SIMPLE"'):<br/>The font tags are handled as follows.
<ul>
 <li>@('<b>..</b>'): Replace each of @('<b>') and @('</b>') by two underscores,
@('__').</li>
 <li>@('<i>..</i>'): Replace each of @('<i>') and @('</i>') by an underscore, @('_').</li>
 <li>@('<em>..</em>'): Replace each of @('<em>') and @('</em>') by an underscore, @('_').</li>
 <li>@('<u>..</u>'): Replace each of @('<u>') and @('</u>') by an underscore, @('_').</li>
 <li>@('<tt>..</tt>'): Just drop @('<tt>') and @('</tt>')</li>
</ul>
</li>

<li>@('"PLAIN"'):<br/>The font tags are all dropped; that is, the text is
printed as though the tags were not present.</li>

</ul>

<p>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.</p>

<ul>

<li>For the built-in @(':doc') command this behavior cannot be customized.</li>

<li>However, behavior is fully customizable for the &ldquo;modified
@(':doc')&rdquo; command, which is the @(':doc') command provided by @(see
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 @(tsee setenv$)
inside ACL2, e.g., @('(setenv$ "ACL2_XDOC_TAGS" "PLAIN")').</li>

<li>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.</li>

</ul>

<h3>Design notes</h3>

<p>Here we make a few observations about why font tags are handled as they
are.</p>

<ul>

<li>We have seen that for a fancy environment, text within
<tt>&lt;b&gt;...&lt;/b&gt;</tt> is rendered not only as bold but also as red.
That is because bold text does not often show up clearly.</li>

<li>The use of &lsquo;@('*')&rsquo; 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.</li>

<li>The use of a grey background (which may technically be called
&ldquo;white&rdquo;, 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.</li>

</ul>

<h3>Changing the default builds of text-based manuals</h3>

<p>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.</p>

<p>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 @(see 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.</p>

<ul>

<li>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).</li>

<li>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.</li>

</ul>

<p>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.</p>

<p>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.</p>

<p>The ACL2+books rendered manual is file
@('books/system/doc/rendered-doc-combined.lsp'), and there is also an
&ldquo;ACL2 only&rdquo; 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/').</p>

@({
(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)
})

<p>For example, suppose you want underscores to surround text that is marked
with @('<i>'), so that for example &ldquo;&lt;i&gt;italicized
text&lt;/i&gt;&rdquo; is printed as &ldquo;_italicized text_&rdquo;.  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 @(see acl2::community-book) @('"xdoc/init"') as
discussed above, so that you are using the modified @(':doc') command.</p>

<p>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 @(see 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.</p>")

(defxdoc save
  :short "Saves the XDOC database into files for web browsers, etc."
  :long "<p>Once you have documented your books with @(see defxdoc), you may
wish to create a manual that can be viewed from a web browser or from the
acl2-doc Emacs-based browser (see @(see acl2::acl2-doc)).</p>

<h4>Basic Example</h4>

@({
 ;; my-manual.lisp - a book that creates a manual
 (in-package "MYPKG")

 (include-book "my-library1") ;; load books I want in the manual
 (include-book "my-library2") ;; (documented with xdoc)

 (include-book "xdoc/save" :dir :system)  ;; load xdoc::save

 (defxdoc acl2::top           ;; create a "top" topic
   :short "My Manual"
   :long "<p>This manual explains how to use my books...</p>")

 (xdoc::save "./mylib-manual" :error t)  ;; write the manual
})

<p>Notes about this example:</p>

<ul>

<li>The @('xdoc::save') command will export all currently-loaded, documented
topics.  Because of this, you can mostly control what goes into the manual
<b>just by including books</b>, but see below for additional notes about how to
control what goes in a manual.</li>

<li>The @('save') command is a macro that expands into @(see
acl2::embedded-event-form)s.  Typically, you just put it into a new book (e.g.,
@('my-manual.lisp') above) so that your manual will be regenerated as part of
building your project.</li>

<li>The @('save') requires certain <see topic='@(url defttag)'>trust
tags</see>.  You may need to enable trust tags in your build system to certify
the @('my-manual') book.  For instance, @('cert.pl') users may need a
@('.acl2') file with a line such as:

@({
    ; cert-flags: ? t :ttags :all
})</li>

<li>After saving a manual, you should be able to view it by going to, e.g.,
@('mylib-manual/index.html') in your web browser.  If you want to share your
manual with others, you should read about @(see deploying-manuals).</li>

</ul>


<h4>General Form</h4>

@({
    (save <target-dir>
          [:redef-okp  bool]               ;; default is nil
          [:zip-p      bool]               ;; default is t
          [:logo-image path]               ;; default is nil
          [:error      bool]               ;; default is nil
          [:broken-links-limit nil-or-nat] ;; default is nil
          )
})

<p>The only (required) argument to the @('save') command is the name of a
directory where the want the manual to go.  All arguments are evaluated.
As might be expected:</p>

<ul>

<li>If the target directory does not exist, it will be created.</li>

<li>If the target directory already exists, it <color rgb="#ff0000">will be
overwritten</color>.  (<b><color rgb="#ff0000">WARNING</color></b>: So, the
target directory should not be one containing files that you want to keep, such
as the directory containing the file that invokes @('xdoc::save'), or its
parent directory (or its parent, etc.).)</li>

</ul>

<h5>Option Summary</h5>

<dl>

<dt>@('redef-okp')</dt>

<dd>By default, the @('save') command will complain if any topic is defined
more than once.  This is often annoying when you are developing books,
especially if your books are slow to certify and you don't want to have your
build fail just because of a documentation problem.  So, if you want to
suppress this error (and turn it into a printed warning), you can set
@(':redef-okp t').</dd>

<dt>@('zip-p')</dt>

<dd>To support the <a href='download/'>Download this Manual</a>
feature (normally accessed from the toolbar button) the @('save') command will
zip up the manual to create @('.tar.gz'), @('.tar.bz2'), and @('.zip') files.
If you don't care about generating these files and want to avoid the time to
build them, you can set @(':zip-p nil').</dd>

<dt>@(':logo-image')</dt>

<dd>You can provide a custom image to use as the logo for the @(see top) topic.
The path you provide should be relative to whatever book contains the @('save')
command.</dd>

<dt>@(':error')</dt>

<dd>The value is @('t') or @('nil'), to indicate whether or not (respectively)
to cause an error upon encountering a syntax error in xdoc source (marked with
"xdoc error").</dd>

<dt>@(':broken-links-limit')</dt>

<dd>The value is @('nil') by default.  Otherwise, it is a natural number
specifying the maximum allowed number of broken links; if the ``broken topic
link'' report shows more broken links than that limit, an error occurs.</dd>

</dl>


<h3>Avoiding Unwanted Documentation</h3>

<p>By default, the @('save') command will generate a manual that covers the
documentation for all books that you have loaded.  This usually works well
as long as you know all of the books that you need to include.</p>

<p>One caveat is that @('xdoc/save') includes some supporting books that are,
themselves, documented.  Accordingly, you may find that your manual includes
documentation from libraries like @(see acl2::std/strings) and @(see
oslib::oslib) in your output even if you haven't loaded these libraries
yourself.  If you really want precise control over what goes into your manual,
then, you may want to do something like this:</p>

@({
 ;; nothing-extra-manual.lisp - manual with nothing extra
 (in-package "MYPKG")

 (include-book "my-library1") ;; load books I want in the manual
 (include-book "my-library2") ;; (documented with xdoc)

 (make-event ;; save current documentation
  `(defconst *just-my-documentation*
     ',(xdoc::get-xdoc-table (w state))))

 (include-book "xdoc/save" :dir :system)

 ;; clobber any docs that were added due to xdoc/save
 (table xdoc::xdoc 'xdoc::doc *just-my-documentation*)

 (defxdoc acl2::top           ;; create a "top" topic
   :short "My Manual"
   :long "<p>This manual explains how to use my books...</p>")

 (xdoc::save "./mylib-manual" :error t)
})")

(defxdoc save-rendered
  :parents (xdoc)
  :short "Saves the XDOC database into files for the acl2-doc browser"
  :long "<p>Also see @(see save-rendered-event) for a corresponding macro that
  provides additional functionality.</p>

 @({
 General Form:

 (save-rendered outfile
                header
                topic-list-name
                error
                write-acl2-doc-search-file
                state)
 })

 <p>where @('outfile') is the pathname for the output file containing rendered
 documentation, @('header') is to be written to the top of
 @('outfile') (typically as a comment), and the value of @('topic-list-name')
 is a symbol that can be the first argument of @(tsee defconst), hence of the
 form @('*c*').  The value of @('error') should be @('t') or @('nil') to
 indicate whether or not (respectively) to cause an error upon encountering a
 syntax error in xdoc source (marked by "xdoc error").  When the value of
 @('write-acl2-doc-search-file') is not @('nil'), then a file
 @('"acl2-doc-search"') is written, to be used for speeding up @(see
 acl2::acl2-doc) search commands.</p>

 <p>Upon success, the call displayed above returns the error-triple @('(mv
 nil (value-triple :ok) state)'); probably the value is unimportant except that
 it allows an @('xdoc::save-rendered') call to be placed inside
 @('make-event'), as displayed below.</p>

 <p>For example, the following form may be found in community book
 @('books/doc/top.lisp').  Its evaluation creates the output file
 @('books/system/doc/rendered-doc-combined.lsp"').  That file starts with a
 comment from the string, @('*rendered-doc-combined-header*'), then contains
 @('(in-package "ACL2")'), and concludes with a form @('(defconst
 *ACL2+BOOKS-DOCUMENTATION* '<big-alist>)'), where @('<big-alist>') is an alist
 representing the XDOC database.</p>

 @({
 (make-event
  (time$
   (xdoc::save-rendered
    (extend-pathname (cbd)
                     "../system/doc/rendered-doc-combined.lsp"
                     state)
    *rendered-doc-combined-header*
    '*acl2+books-documentation*
    t ; cause error upon encountering xdoc error
    state)))
 })

 <p>The output file is typically used by the acl2-doc Emacs-based browser for
 XDOC.  See @(see acl2::acl2-doc), specifically the discussion of custom
 manuals, which explains that the @('filename') argument of Emacs function
 @('extend-acl2-doc-manual-alist') is exactly the output file created by
 @('xdoc::save-rendered').</p>")

(defxdoc save-rendered-event
  :parents (xdoc)
  :short "Event that invokes @(tsee save-rendered), supporting extra functionality"
  :long "<p>See @(see save-rendered) for relevant background.</p>

 @({
 General Form:

 (save-rendered-event outfile
                      header
                      topic-list-name
                      error
                      &key
                      script-file script-args timep write-acl2-doc-search-file)
 })

 <p>where the four required arguments correspond to the same arguments of
 @(tsee save-rendered).  Although @('save-rendered') and
 @('save-rendered-event') have similar effects &mdash; indeed,
 @('save-rendered-event') invokes @('save-rendered') with the same first four
 arguments &mdash; @('save-rendered-event') is a macro that generates an event
 form (using @(tsee make-event)) that can be placed in a book.  All arguments
 are evaluated.  The keyword arguments of @('save-rendered-event') provide
 additional functionality, as follows.</p>

 <p>Suppose @(':script-file') is supplied with a non-@('nil') value.  Then
 there must be an active trust tag (see @(see defttag).  The value of
 @(':script-file') should be a string that names a file to be executed as a
 shell command, using @(tsee sys-call).  The argument list of that command is
 provided by the value of @(':script-args').  For an example, see the call of
 @('xdoc::save-rendered-event') in community book @('doc/top.lisp').</p>

 <p>If @(':timep') is non-@('nil') then the entire computation will be wrapped
 in a call of @(tsee time$).</p>

 <p>The value of keyword option @(':write-acl2-doc-search-file'), which is
 @('nil') by default, is passed directly to the corresponding parameter of
 @(tsee save-rendered).</p>")

(defxdoc deploying-manuals
  :parents (save)
  :short "How to distribute XDOC manuals for other people to use."
  :long "<p>After you have documented your books with XDOC and created a
manual, you may wish to share your manual with coworkers, collaborators,
customers, sponsors, etc.  The best way to do this may depend on many
factors.</p>

<p>By default, the manuals created by @(see save) use only client-side
JavaScript code.  This makes deployment very easy: you can just copy the files
to wherever you like, and you don't even need a web server.</p>

<p>This approach&mdash;just copying the default manual&mdash;is well-suited
for:</p>

<ul>
<li>Browsing from your local hard-drive, or</li>
<li>Browsing from a fast NFS drive or intranet server</li>
</ul>

<p>But the default manuals will <b>perform badly on slow connections</b>.  So,
if your users are going to read the manual over, e.g., VPNs or public web
sites, then you may wish to read on.</p>


<h3>Server-Supported Manuals</h3>

<p>The basic reason that the default manuals are slow is that they work by
simply loading the data for <b>every</b> topic, at startup.  As of the time of
writing (July 2025), this comes to around 310 MB of data for the basic
@('doc/top.lisp') manual.  It's no big deal to load 310 MB from a local hard
drive or a fast intranet connection, but it can be quite slow over the
internet.</p>

<p>The XDOC manuals created by @('save') can be reconfigured to just load the
@(':long') sections as they are accessed.  This results in a much
faster-loading manual, and is how, for instance, the online XDOC manual at
Centaur was deployed.</p>

<p>This option requires a small amount of configuration, and you may need to
coordinate with your network administrator to get certain software
installed.</p>

<p>If you want to use our scripts directly, you will need a web server that
supports <a href='http://www.perl.org'>Perl</a> scripts with the CGI, DBI, and
DBD::SQLite modules installed.  If for some reason this poses a problem, you
may find that you can easily port these scripts to other popular languages,
like PHP or Ruby, with SQLite support.</p>


<h4>Step 1: Create the Database</h4>

<p>In the manual directory you created with the @(see save) command, you should
find a Perl script named @('xdata2sql.pl').  When you run this script, you
should see something like the following output:</p>

@({
$ cd my-library/manual
$ perl xdata2sql.pl
-------------------------------------------------------------------------------

xdata2sql.pl: Convert xdata.js into xdata.db (an sqlite3 database)

   NOTE: Most folks don't need to run this at all!
         If you just want to:
          - browse an XDOC manual on your local hard drive, or
          - share an XDOC manual on your fast intranet
         then ignore this script and just see index.html.

The main use for this script is to share XDOC manuals on the internet.  In this
scenario, just having the web browser load in the entire (generally 20+ MB)
xdata.js file is not very practical, because some users will have slow
connections and will take too long to load the file.

There are many ways to solve this.  Our approach is to convert xdata.js into an
sqlite3 database, and then use a server-side script that will allow us to
access topics only as they are requested.

-------------------------------------------------------------------------------

; Converting xdata.js

; Reading file
; Checking file
; Parsing JSON data.
; Creating new xdata.db.
; Creating xdoc_data table.
; Populating xdoc_data table.
; All done.

To actually use the database, see xdataget.pl.
})

<p>After this step, you should have a new file named @('xdata.db') in your
manual directory.  This is an SQLite3 database that has the information for
your XDOC topics.  It should be roughly as large as @('xdata.js').</p>

<p>If you are missing some required Perl modules, then instead of the above
output you may see a message such as</p>

@({
    Can't locate DBI.pm in @INC ...
})

<p>In this case, you may need to ask your systems administrator to install the
missing modules.</p>


<h4>Step 2: Set up the Web Server</h4>

<p>Once you have created the @('xdata.db') file, you will need to copy both it
and a different script, @('xdataget.pl'), to some directory in your web
server.  If @('xdata.db') is not placed in the same directory as
@('xdataget.pl'), @('xdataget.pl') will not be able to find it.</p>

<p>Typically, for @('xdataget.pl') to work at all, it will need to have its
executable bit set, and it may need to be in a special directory within your
web server, typically named @('cgi-bin').</p>

<p>To make sure the script is working, you should now load it in your web
browser by going to, e.g., @('http://my-server/cgi-bin/xdataget.pl').  If
everything is working, you should see a page that looks like this:</p>

@({
     {"results":[

     ]}
})

<p>If, instead, you see a message like <i>Internal Server Error</i>, then you
may have a permissions problem, or your web server's version of Perl may be
missing a require library, or something else may be wrong; ask your systems
administrator for help.</p>

<p>You may also wish to load, e.g.,:</p>

@({
    http://my-server/cgi-bin/xdataget.pl?keys=ACL2____TOP
})

<p>and make sure that you can see some text from your top topic.</p>


<h4>Step 3: Configure the Manual to use the Server</h4>

<p>The final step is to edit the file @('config.js') in your manual.
This file contains comments with the example syntax.  Basically you
just need to change:</p>

@({
    var XDATAGET = "";
})

<p>To have the right URL for your xdataget.pl script, e.g., into:</p>

@({
    var XDATAGET = "http://my-server/cgi-bin/xdataget.pl";
})

<p>At this point, your manual should load topic data dynamically as needed.
The result should be much faster for users on slow connections.</p>

<h4>Deploying the SEO Manual</h4>

<p>There is also an SEO variant of the server-supported manual which is more
accessible to web crawlers (but less accessible to humans).  To deploy this
manual, repeat the steps above but with the @('xdata2sql4seo.pl') script, which
will produce @('xdata-seo.db').  You will also need to deploy to a server which
supports PHP.</p>

<p>The SEO variant of the manual is intended to be deployed in addition to the
regular server-supported manual, not to replace it.  The SEO variant is not
intended for typical use and is only provided to allow search engines to index
the site.</p>")

(defxdoc emacs-links
  :short "Instructions for integrating XDOC web pages with <a
  href='http://www.gnu.org/software/emacs/'>Emacs</a>."
  :long "<p>@(csee preprocessor) directives such as @('@(def get-xdoc-table)')
result in the introduction of special links for Emacs.  Here's what these links
look like:</p>

@(def get-xdoc-table)

<p>Depending on your environment, it <b>may</b> be easy to configure your web
browser so that clicking on these links will cause Emacs to directly open up
the appropriate source file and jump to the named function.</p>

<p>The basic idea is:</p>

<ul>

<li>Each Emacs link generates a <a
href='https://en.wikipedia.org/wiki/Data_URI_scheme'>Data URIs</a> that tells
your web browser to download a new, generated file whose <a
href='https://en.wikipedia.org/wiki/Internet_media_type'>MIME type</a> is
@('application/x-acl2-xdoc-link').</li>

<li>You configure your web browser to send @('application/x-acl2-xdoc-link')
files to Emacs.</li>

<li>You configure your Emacs to carry out a tags search instead of loading
these files.</li>

</ul>

<p>The net effect is that clicking on these links will send you directly to the
desired function in the source code.  This is <b>really slick</b> if you can
get it working.</p>


<h2>Configuring Emacs</h2>

<h4>Loading the XDOC Elisp</h4>

<p>The XDOC directory includes a file called @('xdoc.el'), which tells emacs
what to do with these xdoc-link files.  To tell emacs to load this file at
startup, you can just add a command to your @('.emacs') file like:</p>

@({
 (load "/path/to/acl2/books/xdoc/xdoc.el")
})

<p>This file will be loaded automatically if you load the file of emacs
utilities that comes with ACL2:</p>

@({
 (load "/path/to/acl2/emacs/emacs-acl2.el")
})

<h4>Managing your TAGS tables</h4>

<p>For emacs to make sense of the links you follow, it will need to have the
appropriate <a
href="https://www.gnu.org/software/emacs/manual/html_node/emacs/Tags-Tables.html">tags
tables</a> loaded for all of the libraries you are using.</p>

<p>If you aren't familiar with tags, you basically just need to:</p>

<ul>

<li>Occasionally generate @('TAGS') files for your libraries, using the command
@('etags *.lisp') or similar.</li>

<li>Tell Emacs to "visit" these tags tables with @('visit-tags-table').</li>

</ul>

<h5>Jared's Approach:</h5>

<ul>

<li>I add a @('TAGS') target to my Makefiles, so that when I build my library
the @('etags *.lisp') command is re-run and the @('TAGS') file is kept up to
date.  The Makefile syntax is:

@({
TAGS: $(wildcard *.lisp)
      etags *.lisp
})</li>

<li>Then, in my @('.emacs') file, I have a series of commands like the
following:

@({
 (ignore-errors (visit-tags-table "/path/to/acl2/TAGS"))
 (ignore-errors (visit-tags-table "/path/to/acl2/books/xdoc/TAGS"))
 (ignore-errors (visit-tags-table "/path/to/my/stuff/TAGS"))
})

This ensures that the relevant @('TAGS') files are loaded every time I start
Emacs.  The use of @('ignore-errors') prevents Emacs from complaining if one of
these @('TAGS') files was deleted in a "make clean" or similar.</li>

<li>One final addition to the @('.emacs') file is:

@({
 (setq tags-revert-without-query t)
})

which tells Emacs to go ahead and reload these files when they are rebuilt by
Make, instead of prompting you if you want to reload them.</li>

</ul>


<h4>Setting up Emacsclient (recommended)</h4>

<p>You can set things up so that links open up in <b>new instances</b> of
Emacs, or in <b>new buffers</b> of an already-running Emacs.</p>

<p>If you want everything to open up in a new instance of Emacs, you can skip
this section.  But I prefer to use a single Emacs for everything, and just have
links open up in new buffers.</p>

<p>This is quite easy.  First, add @('(server-start)') to your @('.emacs') file
and restart Emacs.</p>

<p>Next, to ensure everything is working properly, launch a separate terminal
and type:</p>

@({
emacsclient --no-wait my-file
})

<p>If all is well, @('my-file') will be loaded into your already-running emacs
as a new buffer.</p>



<h2>Configuring the Web Browser</h2>

<p>The last thing we need to do is instruct your web browser to send xdoc-link
files to Emacs.</p>

<p>How to do this depends on your web browser and/or operating system.  In some
cases it may be hard to pass command-line options to emacs directly, so you may
find it useful to use the script @('emacsclient-wrapper.sh'), found in the xdoc
directory.</p>

<p>The basic starting point is probably to try to click on an emacs link like
@(srclink append) and try to tell your browser to open it with the
@('emacsclient-wrapper.sh') script.  If your browser opens it with some other
program, you might need to edit the default file associations of your operating
system or window manager.</p>")

(defxdoc extract-keyword-from-args
  :parents (defsection)
  :short "Get the value for a keyword argument like @(':foo value')."
  :long "<p>@(call extract-keyword-from-args) is given @('kwd'), which should
be a keyword symbol, and a list of @('args') which are typically the @('&rest
args') given to a macro.  It scans the list of @('args'), looking for the
indicated keyword, and returns @('(kwd . value)'), or @('nil') if no such
keyword is found.  For instance,</p>

@({
 (extract-keyword-from-args :bar '(:foo 3 :bar 5 :baz 7))
   -->
 (:bar . 5)
})

<p>This function is mainly useful for writing macros that mix @('&rest') parts
with keyword arguments.  See also @(see throw-away-keyword-parts).</p>

@(def extract-keyword-from-args)")

(defxdoc throw-away-keyword-parts
  :parents (defsection)
  :short "Throw away any keyword arguments and their values from a macro
argument list."
  :long "<p>@(call throw-away-keyword-parts) is given a list of arguments that
are typically the @('&rest args') given to a macro.  It scans the arguments for
any keyword symbols such as @(':foo'), and throws away both the keyword and the
argument that follows it.  For instance,</p>

@({
 (throw-away-keyword-parts '(x y z :foo 3 :bar 5 blah blah blah))
   -->
 '(x y z blah blah blah)
})

<p>This function is mainly useful for writing macros that mix @('&rest') parts
with keyword arguments.  See also @(see extract-keyword-from-args).</p>

@(def throw-away-keyword-parts)")

(defxdoc defsection
  :short "Fancy @('(encapsulate nil ...)') with a name and @(see xdoc) support."
  :long "<h4>General Form</h4>

@({
 (defsection name
    [:parents   parents]
    [:short     short]
    [:long      long]
    [:autodoc   autodoc]
    [:extension topic]
    [:set-as-default-parent t/nil]
    ... events and commentary ...)
})

<h4>Example</h4>

@({
 (defsection foo
   :parents (parent1 parent2 ...)
   :short "@(call foo) is like @(see bar), but better when..."
   :long "<p>The main differences between @('foo') and @('bar') are ...</p>"

   (defund foo (x) ...)
   (local (in-theory (enable foo)))
   (defthm foo-thm1 ...)
   (defthm foo-thm2 ...)

   "<p>NOTE: the next theorem is really useful, but we keep it disabled
   because it gets too expensive when...</p>"

   (defthmd foo-thm3 ...))
})

<box><p>Note: this example might be better written as a @(see std::define),
which is much like a @('defsection') but has additional features.</p></box>

<h3>Overview</h3>

<p>Like an @(see encapsulate), a @('defsection') introduces a new scope for
@(see local) events.  This is often useful when you are trying to prove a
theorem that requires some lemmas: by proving the lemmas locally, you can
prevent them from affecting the rest of your book.</p>

<p>It is often useful to organize books into sections.  There are a few minor
reasons you might prefer using @('defsection') for this, instead of plain
@('encapsulate')s.  For instance,</p>

<ul>

<li>It is easier to identify in the @(':pbt') history, and</li>

<li>It indents more nicely than @('encapsulate') in a vanilla emacs.</li>

</ul>

<p>But the main reasons to use @('defsection') are its documentation features.
The definitions and theorems within a section can be <b>automatically</b>
included in the documentation page for that section, along with any running
commentary.  This helps to avoid copying-and-pasting code into the manual, and
keeps it up-to-date as the code changes.</p>


<h3>Ordinary Sections</h3>

<p>The @(':parents'), @(':short'), and @(':long') keywords are optional.  If
any of these keywords are provided, they will be used to introduce a @(see
defxdoc) command; otherwise no documentation will be generated.</p>

<p>By default, the @(':long') string you give will be automatically extended
with a "Definitions and Theorems" part that lists all of the (non-local,
non-redundant) definitions and theorems introduced in the section.</p>

<p>For instance, in the above example, the @(':long') field would be extended
with:</p>

@({
 <h3>Definition and Theorems</h3>

 @(def foo)
 @(thm foo-thm1)
 @(thm foo-thm2)

 <p>NOTE: the next theorem is really useful, but we keep it disabled
   because it gets too expensive when...</p>

 @(thm foo-thm3)
})

<p>If you do not want this automatic documentation, you can turn it off with
@(':autodoc nil').</p>

<p>If you want the section name to be the default parent for the encapsulated
events, then you can pass @(':set-as-default-parent t'). Then @('(local
(xdoc::set-default-parents name))') will be inserted at the beginning of the
events, where "name" is the name of the section.</p>

<h3>Extended Sections</h3>

<p>The @(':extension') keyword allows you to say that this section is a
continuation of a previously introduced concept.</p>

<p>When @(':extension topic') is provided, then @('topic') must be the name of
a previously documented @(see xdoc) section, and you are not allowed to use
@(':parents') or @(':short') since the topic already exists.  Note that whereas
topics can have multiple parents, you can only extend a single topic at a
time.</p>

<p>The main purpose of an @(':extension') section is to add additional
documentation, either via the @(':long') string or via the automatic events and
commentary.  The documentation obtained this way is just appended onto the
existing @(':long') for the topic.</p>

<p>For example, say we have already defined the above @('foo') section in some
"basic" book.  We might then want to add some additional "advanced"
theorems about it in some other book.  We could do this via:</p>

@({
 (defsection advanced-theorems-about-foo
   :extension foo

   "<p>Additional theorems are also available in the @('advanced') book.  (We
     don't include these in the basic book since they take a long time to
     prove.)</p>"

   (defthm foo-thm4 ...)
   (defthm foo-thm5 ...))
})

<p>This will result in the commentary and definitions of @('foo-thm4') and
@('foo-thm5') being added onto the end of the documentation for @('foo').</p>")

(defxdoc defsection-progn
  :short "Fancy @('(progn ...)') with a name and @(see xdoc) support."
  :long "<p>The @('defsection-progn') macro is like @(see defsection) except
that it generates @({(progn ...)}) instead of an @({(encapsulate nil ...)})</p>

<p>This has a number of consequences, mostly having to do with the scope of
@('local') events within the section.  In short, a @('defsection-progn') does
not introduce a new local scope, but a @('defsection') does.</p>")

(defxdoc undocumented
  :short "Placeholder for documentation topics that lack good @(':parents')."
  :long "<p>Many @(see acl2::macros) such as @(see std::deflist) and other
@(see acl2::std/util) macros can automatically generate @(see xdoc)
documentation topics.</p>

<p>When someone uses these macros but doesn't give any @(':parents') for the
resulting documentation, we put the resulting documentation here.  This seems
better than just dropping the documentation completely, since at least you can
at least see the boilerplate documentation and any embedded documentation that
the programmer did provide.</p>

<p>As ongoing documentation improvement work, most topics here can benefit from
being given more appropriate @(':parents').</p>")

(defxdoc missing-parents
  :short "Placeholder for documentation topics that lack @(':parents')."
  :long "<p>If a @(see defxdoc) form ends up having no parents, it ends up
being put here.  See also @(see undocumented).</p>

<p>Historic note.  We used to put these topics directly underneath @(see top)
instead.  But we found that during development, this sometimes led to a
strange-looking hierarchy where ``random'' topics were presented as top-level
topics just because they were new or being moved around or because @(see
set-default-parents) forms weren't quite in the right places.  To avoid this,
we now move these topics to @('missing-parents') and print notes about them
when a manual is saved with @(see xdoc::save).</p>")

(defxdoc set-default-parents
  :short "Set up default parents to use for @(see xdoc)."
  :long "<p>When documenting a book of inter-related functions, you may
sometimes wish to use the same @(':parents') across many @(see defxdoc) or
@(see defsection) commands.  This can sometimes get tedious.</p>

<p>The macro @(call set-default-parents) can be used to set up a default list
of parent topics to be automatically used by commands such as @(see defxdoc)
and @(see defsection).</p>

<p>Basic Example:</p>

@({
   (local (set-default-parents fox-p))

   (defxdoc make-fox           ;; use default :parents, (fox-p)
     :short ...
     :long ...)

   (defsection feed-fox        ;; use default :parents, (fox-p)
     :short ...
     :long ...)

   (defsection chase-mouse     ;; use explicit :parents, (fox-p mouse-p)
     :parents (fox-p mouse-p)
     :short ...
     :long ...)

   (local (set-default-parents fox-p hawk-p))

   (defsection bother-hawk     ;; use default :parents, (fox-p hawk-p)
     :short ...
     :long ...)

   (local (set-default-parents nil))

   (defxdoc zebra-p            ;; use default :parents, nil
     :short ...
     :long ...)
})

<p>Note that @('set-default-parents') is just a macro that expands to a @(see
table) event.  It's good practice to only <b>locally</b> set the default
parents&mdash;otherwise the default parents can "leak" from your book and
lead you to inadvertently set the parents of other, unrelated topics.</p>")

(defxdoc xdoc-extend
  :short "Extend an existing XDOC topic with additional content."
  :long "<p>Basic example:</p>

@({
     (defxdoc foo
       :short "Example of xdoc-extend."
       :long "<p>Foo is very important.</p>")

     (xdoc::xdoc-extend foo
       "<p>Note: you can't use Foo with Bar.</p>")
})

<p>is roughly equivalent to just writing:</p>

@({
     (defxdoc foo
       :short "Example of xdoc-extend."
       :long "<p>Foo is very important.</p>
               <p>Note: you can't use Foo with Bar.</p>")
})

<p>@(call xdoc-extend) requires that @('name') is an existing XDOC topic, e.g.,
it may have been introduced with @(see defxdoc), @(see defsection), or similar.
We just look up that topic and extend its @(':long') string by appending the
new @('long') fragment to it.</p>

<p>This mechanism is barbaric and fragile.  For instance:</p>

<ul>

<li>You can't put the new content anywhere except at the end of the current
@('long') string.  (But see @(see xdoc-prepend) if you want to extend the
beginning of a topic).</li>

<li>If you extend a topic several times in different books, the resulting text
may differ depending on the particular @(see include-book) order that happens
to be used.</li>

</ul>

<p>Nevertheless, judiciously used, it can be a useful tool for connecting
together related content that must be kept in separate files, e.g., for
bootstrapping or other reasons.</p>")

(defxdoc xdoc-prepend
  :short "Extend an existing XDOC topic with additional content, at the front."
  :long "<p>@(call xdoc-prepend) is very much like @(see xdoc-extend), except
that it extends the @(':long') string for @('name') at the front, instead of at
the back.</p>

<p>Basic example:</p>

@({
     (defxdoc foo
       :short "Example of xdoc-prepend."
       :long "<p>Foo is very important.</p>")

     (xdoc::xdoc-prepend foo
       "<p>Never use Foo, use Bar instead!</p>")
})

<p>is roughly equivalent to just writing:</p>

@({
     (defxdoc foo
       :short "Example of xdoc-prepend."
       :long "<p>Never use Foo, use Bar instead!</p>
               <p>Foo is very important.</p>")
})

<p>See @(see xdoc-extend) for related commentary.</p>")

(defxdoc order-subtopics
  :short "Control the ordering of subtopics in the XDOC display."
  :long "<p>@(call order-subtopics) allows you to specify what order the
subtopics of @('name') will be presented in.  For instance:</p>

@({
    (xdoc::order-subtopics mini-tutorial
      (example syntax semantics gotchas references))
})

<p>By default, XDOC shows subtopics in an alphabetical order.  For most
reference-manual material this is generally fine.  But, especially for tutorial
guides, you sometimes intend your topics to be read in some particular order,
and alphabetizing things gets in the way.</p>

<p>The @('order-subtopics') command lets you specify the exact subtopic
ordering that should be used for a particular topic.  One general form is:</p>

@({
    (xdoc::order-subtopics parent
      (subtopic1 subtopic2 ... subtopicn))
})

<p>You don't have to give a complete order.  Any subtopics that aren't
mentioned will be listed last, in the usual alphabetical order.</p>

<p>A second general form has an optional argument of @('t').  This specifies
that the order for unspecified child topics is the order in which the topics
were defined, rather than alphabetical.</p>

@({
    (xdoc::order-subtopics parent
      (subtopic1 subtopic2 ... subtopicn)
      t)
})

<p>A special case of that second general form lists no subtopics, thus
specifying simply that all children are to be listed in the order in which they
were defined.</p>

@({
    (xdoc::order-subtopics parent
      nil
      t)
})

<p>We require @('parent') to refer to some defined topic, but the subtopics
don't need to be defined at @('order-subtopics') time.  This makes it easy to
keep the subtopic ordering close to the defxdoc command, e.g., you can
write:</p>

@({
     (defxdoc mini-tutorial ...))
     (order-subtopics mini-tutorial (example syntax ...))

     (defxdoc example ...)
     (defxdoc syntax ...)
})

<p>We do at least warn about undefined topics when you @(see save) a
manual.</p>")

(defxdoc xdoc-tests
  :short "Topics that exist only to test XDOC functionality.")

(local (set-default-parents xdoc-tests))

(defxdoc entities
  :parents (xdoc xdoc-tests)
  :short "HTML entity support in XDOC."
  :long "<h3>Entities that XDOC allows:</h3>

<p>Normal XML entities:</p>

<ul>
<li>@('&amp;')   becomes &amp;</li>
<li>@('&lt;')    becomes &lt;</li>
<li>@('&gt;')    becomes &gt;</li>
<li>@('&quot;')  becomes &quot;</li>
<li>@('&apos;')  becomes &apos;</li>
</ul>

<p>Additional basic and math entities allowed by XDOC:</p>

<ul>
<li>@('&nbsp;')  becomes &nbsp; (that is, a single space)</li>
<li>@('&mdash;') becomes &mdash;</li>
<li>@('&larr;')  becomes &larr;</li>
<li>@('&rarr;')  becomes &rarr;</li>
<li>@('&harr;')  becomes &harr;</li>
<li>@('&lang;')  becomes &lang;</li>
<li>@('&rang;')  becomes &rang;</li>
<li>@('&hellip;') becomes &hellip;</li>
<li>@('&lsquo;') becomes &lsquo;</li>
<li>@('&rsquo;') becomes &rsquo;</li>
<li>@('&ldquo;') becomes &ldquo;</li>
<li>@('&rdquo;') becomes &rdquo;</li>
<li>@('&and;')   becomes &and;</li>
<li>@('&or;')    becomes &or;</li>
<li>@('&not;')   becomes &not;</li>
<li>@('&ne;')    becomes &ne;</li>
<li>@('&le;')    becomes &le;</li>
<li>@('&ge;')    becomes &ge;</li>
<li>@('&mid;')   becomes &mid;</li>
<li>@('&times;') becomes &times;</li>
</ul>

<p>Capitalized Greek letters:</p>

<ul>
<li>@('&Alpha;') becomes &Alpha;</li>
<li>@('&Beta;') becomes &Beta;</li>
<li>@('&Gamma;') becomes &Gamma;</li>
<li>@('&Delta;') becomes &Delta;</li>
<li>@('&Epsilon;') becomes &Epsilon;</li>
<li>@('&Zeta;') becomes &Zeta;</li>
<li>@('&Eta;') becomes &Eta;</li>
<li>@('&Theta;') becomes &Theta;</li>
<li>@('&Iota;') becomes &Iota;</li>
<li>@('&Kappa;') becomes &Kappa;</li>
<li>@('&Lambda;') becomes &Lambda;</li>
<li>@('&Mu;') becomes &Mu;</li>
<li>@('&Nu;') becomes &Nu;</li>
<li>@('&Xi;') becomes &Xi;</li>
<li>@('&Omicron;') becomes &Omicron;</li>
<li>@('&Pi;') becomes &Pi;</li>
<li>@('&Rho;') becomes &Rho;</li>
<li>@('&Sigma;') becomes &Sigma;</li>
<li>@('&Tau;') becomes &Tau;</li>
<li>@('&Upsilon;') becomes &Upsilon;</li>
<li>@('&Phi;') becomes &Phi;</li>
<li>@('&Chi;') becomes &Chi;</li>
<li>@('&Psi;') becomes &Psi;</li>
<li>@('&Omega;') becomes &Omega;</li>
</ul>

<p>Lower case Greek letters:</p>

<ul>
<li>@('&alpha;') becomes &alpha;</li>
<li>@('&beta;') becomes &beta;</li>
<li>@('&gamma;') becomes &gamma;</li>
<li>@('&delta;') becomes &delta;</li>
<li>@('&epsilon;') becomes &epsilon;</li>
<li>@('&zeta;') becomes &zeta;</li>
<li>@('&eta;') becomes &eta;</li>
<li>@('&theta;') becomes &theta;</li>
<li>@('&iota;') becomes &iota;</li>
<li>@('&kappa;') becomes &kappa;</li>
<li>@('&lambda;') becomes &lambda;</li>
<li>@('&mu;') becomes &mu;</li>
<li>@('&nu;') becomes &nu;</li>
<li>@('&xi;') becomes &xi;</li>
<li>@('&omicron;') becomes &omicron;</li>
<li>@('&pi;') becomes &pi;</li>
<li>@('&rho;') becomes &rho;</li>
<li>@('&sigma;') becomes &sigma;</li>
<li>@('&tau;') becomes &tau;</li>
<li>@('&upsilon;') becomes &upsilon;</li>
<li>@('&phi;') becomes &phi;</li>
<li>@('&chi;') becomes &chi;</li>
<li>@('&psi;') becomes &psi;</li>
<li>@('&omega;') becomes &omega;</li>
</ul>

<p>Capitalized letters with diacritics:</p>

<ul>
<li>@('&Ccedil;') becomes &Ccedil;</li>
<li>@('&Aacute;') becomes &Aacute;</li>
<li>@('&Agrave;') becomes &Agrave;</li>
<li>@('&Acirc;') becomes &Acirc;</li>
<li>@('&Atilde;') becomes &Atilde;</li>
<li>@('&Auml;') becomes &Auml;</li>
<li>@('&Aring;') becomes &Aring;</li>
<li>@('&Egrave;') becomes &Egrave;</li>
<li>@('&Eacute;') becomes &Eacute;</li>
<li>@('&Ecirc;') becomes &Ecirc;</li>
<li>@('&Euml;') becomes &Euml;</li>
<li>@('&Igrave;') becomes &Igrave;</li>
<li>@('&Iacute;') becomes &Iacute;</li>
<li>@('&Icirc;') becomes &Icirc;</li>
<li>@('&Iuml;') becomes &Iuml;</li>
<li>@('&Ntilde;') becomes &Ntilde;</li>
<li>@('&Ograve;') becomes &Ograve;</li>
<li>@('&Oacute;') becomes &Oacute;</li>
<li>@('&Ocirc;') becomes &Ocirc;</li>
<li>@('&Otilde;') becomes &Otilde;</li>
<li>@('&Ouml;') becomes &Ouml;</li>
<li>@('&Ugrave;') becomes &Ugrave;</li>
<li>@('&Uacute;') becomes &Uacute;</li>
<li>@('&Ucirc;') becomes &Ucirc;</li>
<li>@('&Uuml;') becomes &Uuml;</li>
<li>@('&Aogon;') becomes &Aogon;</li>
<li>@('&Eogon;') becomes &Eogon;</li>
<li>@('&Iogon;') becomes &Iogon;</li>
<li>@('&Uogon;') becomes &Uogon;</li>
<li>@('&Nacute;') becomes &Nacute;</li>
</ul>

<p>Lower case letters with diacritics:</p>

<ul>
<li>@('&ccedil;') becomes &ccedil;</li>
<li>@('&aacute;') becomes &aacute;</li>
<li>@('&agrave;') becomes &agrave;</li>
<li>@('&acirc;') becomes &acirc;</li>
<li>@('&atilde;') becomes &atilde;</li>
<li>@('&auml;') becomes &auml;</li>
<li>@('&aring;') becomes &aring;</li>
<li>@('&egrave;') becomes &egrave;</li>
<li>@('&eacute;') becomes &eacute;</li>
<li>@('&ecirc;') becomes &ecirc;</li>
<li>@('&euml;') becomes &euml;</li>
<li>@('&igrave;') becomes &igrave;</li>
<li>@('&iacute;') becomes &iacute;</li>
<li>@('&icirc;') becomes &icirc;</li>
<li>@('&iuml;') becomes &iuml;</li>
<li>@('&ntilde;') becomes &ntilde;</li>
<li>@('&ograve;') becomes &ograve;</li>
<li>@('&oacute;') becomes &oacute;</li>
<li>@('&ocirc;') becomes &ocirc;</li>
<li>@('&otilde;') becomes &otilde;</li>
<li>@('&ouml;') becomes &ouml;</li>
<li>@('&ugrave;') becomes &ugrave;</li>
<li>@('&uacute;') becomes &uacute;</li>
<li>@('&ucirc;') becomes &ucirc;</li>
<li>@('&uuml;') becomes &uuml;</li>
<li>@('&aogon;') becomes &aogon;</li>
<li>@('&eogon;') becomes &eogon;</li>
<li>@('&iogon;') becomes &iogon;</li>
<li>@('&uogon;') becomes &uogon;</li>
<li>@('&nacute;') becomes &nacute;</li>
</ul>

<p>Mathematical symbols:</p>

<ul>
<li>@('&forall;') becomes &forall;</li>
<li>@('&exist;') becomes &exist;</li>
<li>@('&empty;') becomes &empty;</li>
<li>@('&isin;') becomes &isin;</li>
<li>@('&notin;') becomes &notin;</li>
<li>@('&prod;') becomes &prod;</li>
<li>@('&sum;') becomes &sum;</li>
</ul>

<h3>A few tests</h3>

<p>Test of `single' and ``double'' smart quoting for legacy topics.</p>

<p>Test of &lsquo;single&rsquo; and &ldquo;double&rdquo; smart quoting for
regular old entities.</p>

<p>Test of <tt>`single' and ``double''</tt> quotes in a @('<tt>') tag and in
a @('<code>') tag:</p>

<code>`single' and ``double''</code>

<p>Test of @(' `single' and ``double'' ') quotes in inline preprocessor stuff,
and in preprocessor blocks here:</p>

@({ `single' and ``double'' quotes ! })

<p>Test of primes in math: @($ foo' $) and</p>

@([ foo' ])

<p>That should probably about do it.</p>")

(order-subtopics xdoc-tests
  (order-test-w order-test-o
    order-test-r
    order-test-z-intentionally-missing
    order-test-k
    order-test-s))

(defxdoc order-test-s :short "S")

(defxdoc order-test-w :short "W")

(defxdoc order-test-r :short "R")

(defxdoc order-test-o :short "O")

(defxdoc order-test-k :short "K")

(defxdoc xdoc-test-order-subtopics-flg
  :short "Parent topic for testing chronological order of subtopics.")

(order-subtopics xdoc-test-order-subtopics-flg
  (order-test-flg-move-to-front)
  t)

(local (set-default-parents xdoc-test-order-subtopics-flg))

(defxdoc order-test-flg-w :short "W")

(defxdoc order-test-flg-o :short "O")

(defxdoc order-test-flg-o :short "O")

(defxdoc order-test-flg-move-to-front
  :short "Move to front")

(defxdoc order-test-flg-r :short "R")

(defxdoc order-test-flg-k :short "K")

(defxdoc order-test-flg-s :short "S")

(local (set-default-parents xdoc))

(defxdoc katex-integration
  :short "Support for LaTeX-like typesetting of mathematics in XDOC
topics. (experimental)"
  :long "<box><p><b>Experimental.</b> This whole thing is experimental.  Jared
reserves the right to decide it is a bad idea and remove support for
it.</p></box>

<p>The <a href='https://www.khanacademy.org/'>Khan Academy</a> has developed a
very nice Javascript library, <a
href='https://github.com/Khan/KaTeX'>KaTeX</a>, for rendering mathematical
formulas in the web browser.  We have now integrated KaTeX into XDOC's fancy
web-based viewer, allowing you to typeset basic formulas.</p>


<h3>Basic Usage</h3>

<box><p><b><color rgb='#ff0000'>ESCAPING WARNING</color></b>. LaTeX-style
formulas may be especially hard to type in ordinary ACL2 string literals
because you have to escape all the backslashes.  For instance, you have to
remember to write @('\\sqrt{x}') instead of @('\sqrt{x}').  You can avoid
this headache by using the @(see acl2::fancy-string-reader). In the rest of
this document, we will use the concrete xdoc syntax without the escapes for
simplicity.</p></box>

<p>To typeset block-style formulas, you can use the @('@([...])') @(see
preprocessor) directive, e.g.,:</p>

@({
    @([
       c = \pm\sqrt{a^2 + b^2}
    ])
})

<p>Produces an indented block of mathematics:</p>

@([
    c = \pm\sqrt{a^2 + b^2}
])

<p>You can also write inline math using @('@($...$)') directive, for
instance:</p>

@({
     The product @($a \times b$) is even.
})

<p>Produces text such as: the product @($a \times b$).</p>


<h3>Tips and Tricks</h3>

<h5>Fast Preview.</h5>

<p>The <a href='formula.html'>KaTeX Preview</a> page lets you interactively
type in your formula and see how it will be typeset.  It may be especially
helpful since KaTeX only supports a particular subset of LaTeX.</p>

<h5>Invalid Formulas.</h5>

<p>Invalid formulas will display as an ugly error message.  For instance, here
is an invalid @('@([ ... ])') style formula:</p>

@([
      { there is no closing brace
])

<p>And here is an invalid @('@($...$)') style formula,
@($
      { there is no closing brace
$), embedded in a paragraph.</p>

<h3>Miscellaneous Notes</h3>

<p>The preprocessor directives expand into @('<math>') and @('<mathfrag>')
tags.  But you will probably want to stick to the preprocessor syntax, rather
than directly using @('<math>') tags, because if you try to use raw @('<math>')
tags then you have to remember to escape XML characters like @('<') with
@('&lt;'), which just isn't very readable.</p>

<p>All of this is fundamentally limited to the web-based viewer.  It seems very
unlikely that @('<math>') formulas will ever look nice when shown at the
terminal with @(':doc') or in the ACL2-Doc Emacs viewer.</p>")

(defxdoc defpointer
  :short "Define an alias for a documentation topic."
  :long "<p>Examples:</p>

@({
    (defpointer acl2s acl2-sedan)
    (defpointer guard-hints xargs t)
})

<p>General Form:</p>

@({
    (defpointer new-topic target-topic [keyword-p])
})

<p>This is a simple macro that expands to a @(see defxdoc) form.  It introduces
a new @(see xdoc) topic, @('new-topic'), that merely links to
@('target-topic').  The new topic will only be listed under @(see
pointers).</p>

<p>A common practice when documenting keyword symbols is to create a
doc topic in in the "ACL2" package or some other relevant package,
rather than the "KEYWORD" package to which the keyword symbol
rightfully belongs.  In keeping with this practice, the @('keywordp')
argument to @('defpointer'), if non-nil, adds a clarification that the
doc topic is really about the keyword symbol with the same name as
@('new-topic'), rather than @('new-topic') itself.</p>")

(defxdoc add-resource-directory
  :short "Tell @(see xdoc) about directories of resources (e.g., images, PDF
files, etc.) that should be copied into manuals."
  :long "<p>Occasionally you may wish to include images or other files within
an XDOC documentation topic.  For this to work, XDOC's @(see save) command
needs to know about these files so that it can copy them into the manual it
produces.  The @('add-resource-directory') command lets you tell XDOC which
directories to copy and what to name them.</p>

<h3>Example</h3>

<p>Suppose that in the @('vl') library there are some images that we want to
include in the manual.  We can put these images into a directory, say
@('images'), and then do:</p>

@({
    (xdoc::add-resource-directory "vl" "images")
})

<p>This will cause the @(see xdoc::save) command to copy everything from the
@('images') directory into the @('res/vl') directory of our manual.  To refer
to these images, we can then write @(see markup) such as:</p>

@({
    <img src="res/vl/logo.jpg"/>
})

<p>These resource directories might also contain files other than images, for
instance, PDF files.  You can at provide hyperlinks to these files by just
linking into the @('res') directory, for instance:</p>

@({
    <a href="res/vl/slides.pdf">See the Slides!</a>
})


<h3>General form</h3>

@({
    (xdoc::add-resource-directory dirname path)
})


<ul>

<li><b>dirname</b> controls where the directory will be placed in within the
manual's @('res') directory.  In the example above, the @('dirname') is
@('"vl"') so the files will be copied into @('"res/vl"').</li>

<li><b>path</b> controls where the files will be copied from.  We recommend
always using a simple path such as the name of an immediate subdirectory.</li>

</ul>

<h3>Working example</h3>

<p>The directory @('books/xdoc/centaur') contains a @('centaur-logo.png') file.
The file @('xdoc/topics.lisp') adds this directory as a resource directory.  If
all is well, you should see the logo below:</p>

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

(add-resource-directory "centaur" "centaur")

(defxdoc testing
  :short "Testing new or revised XDOC strings"
  :long "<p>Contributors to the XDOC manual should check that their XDOC
 strings are well-formed.  This topic shows an easy way to check
 well-formedness of XDOC strings, without the need to build the manual.  Also
 discussed is a way to check for the absence of broken links by building the
 manual.</p>

 <p>To test a topic, first submit a suitable @(tsee in-package) form if
 necessary, and then to test your topic named, say, @('FOO'):</p>

 @({
 (include-book "xdoc/top" :dir :system)
 (defxdoc ...) ; or whatever form you have that includes an XDOC string
 :doc foo ; a bit noisy and slow the first time, but could do this twice
 })

 <p>The output should be free of obvious errors.  Otherwise, you can use the
 error message to debug the error; then submit your form and @(':doc foo')
 again.</p>

 <p>A XDOC feature (the second ``NEW'' feature in the @(see xdoc)
 documentation) avoids the need to invoke @(':doc') explicitly.  In brief: you
 can simply include community-book @('xdoc/debug'), for example by putting its
 include-book form in your acl2-customization file (see @(see
 acl2::acl2-customization)).</p>

 <p>Checking for broken links requires you to build the manual; for
 instructions, see the section ``Building the manual'' in the topic @(see
 acl2::books-certification).  This build will create a file
 @('books/doc/top.cert.out').  Search in that file for the word ``broken'' and
 you will find the following report of a broken link:</p>

 @({
 ;;; ACL2____SOME-BROKEN-LINK:
 ;;;    from ACL2-DOC
 })

 <p>If any other broken links are reported, you can modify the parent topic
 (e.g., @('ACL2-DOC') just above &mdash; but please leave that one in place!)
 to fix the indicated broken link.</p>

 <p>The @(':short') and @(':long') strings, if supplied, must consist entirely
 of standard characters (see @(see standard-char-p)), except that tabs are also
 allowed.  Making this check requires you to build the manual (as described
 just above).</p>")

(defpointer build-the-manual xdoc)