Preprocessor
In addition to its markup language, XDOC includes a
preprocessor which can be used to interpret certain directives of the form
@(...).
Functions and Theorems
To look up function definitions (or pieces of definitions) from the ACL2
world and insert them into your documentation, you can use:
| @(def fn) |
insert the definition of fn
(also works for theorems, macros, ...) |
| @(def? fn) |
Same as @(def fn) but doesn't
produce an error if the definition isn't found |
| @(body fn) |
just the body of fn |
| @(formals fn) |
just the formals of fn |
| @(measure fn) |
just the measure of fn |
| @(call fn) |
a generic function call of fn |
We expect that def and body directives will expand to large code
fragments, so they are automatically wrapped in <code> blocks.
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.
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.
Adding Examples or Code Fragments
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 <.
- @('...') inserts ... into <tt> XDOC tags.
- @({...}) inserts ... into <code> XDOC tags.
These have a special feature for automatically linking to documented topics.
For instance, @('(consp x)') produces (consp x), and
@({ (consp x) }) produces:
(consp x)
Evaluating Lisp from Doc Strings
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:
- @(`(+ 1 2 3)`) produces 6
- @(`(mv 'a 10 state)`) produces (mv a 10 state)
- @(`acl2::*pkg-witness-name*`) produces "ACL2-PKG-WITNESS"
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:
(nil nil nil nil nil nil nil nil nil nil
nil nil nil nil nil nil nil nil nil nil
nil nil nil nil nil nil nil nil nil nil
nil nil nil nil nil nil nil nil nil nil
nil nil nil nil nil nil nil nil nil nil
nil nil nil nil nil nil nil nil nil nil
nil nil nil nil nil nil nil nil nil nil
nil nil nil nil nil nil nil nil nil nil
nil nil nil nil nil nil nil nil nil nil
nil nil nil nil nil nil nil nil nil nil)
(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 < b")`) produces
a < b.
Note that it is quite easy to use :raw incorrectly; you have to escape
things properly yourself!
Emacs Links
The @(srclink name) directive inserts a source-code link for users who
have configured their web browser as described in emacs-links. For
documentation in the acl2-doc browser 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.
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 defxdoc, which often are
written using backquote and hence do not display nicely.
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."
Documentation Links
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, in lower 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.
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:
<see topic="mangled-topic-name">printed-topic-name</see>
Where:
- mangled-topic-name is a canonical, url/file-name friendly,
human-hostile mangling of name's package and symbol names, and
- printed-topic-name is an XML-escaped variant of name, e.g., where
< becomes <, etc.; depending on the package of the current topic's
name, it may or may not include the package portion of name.
So, to support custom links, we provide
- @(url name), which expands to mangled-topic-name
- @(sym name), which expands to printed-topic-name
- @(csym name), like sym, but with the first letter capitalized
You can use these to write your own <see> tags. You should probably
never write a <see> tag yourself without using @(url ...).
Some examples:
- @(url defxdoc) expands to ACL2____DEFXDOC
- @(sym defxdoc) expands to defxdoc
- @(csym defxdoc) expands to Defxdoc
Escaping of @
Since @( is intercepted by the preprocessor, you may occasionally need
to escape it. You can write @@ to generate a single @ sign.
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.
