Major Section: DOCUMENTATION
ACL2 documentation strings make special use of the tilde character (~). In particular, we describe here a ``markup language'' for which the tilde character plays a special role. The markup language is valuable if you want to write documentation that is to be displayed outside your ACL2 session. If you are not writing such documentation, and if also you do not use the character `~', then there is no need to read on.
Three uses of the tilde character (~) in documentation strings are as follows. Below we explain the uses that constitute the ACL2 markup language.
Indicates the end of a documentation section; see doc-string.
Indicates the literal insertion of a tilde character (~).
This directive in a documentation string is effective only during the processing of part 2, the details (see doc-string), and controls how much is shown on each round of
moreprocessing when printing to the terminal. If the system is not doing
moreprocessing, then it acts as though the ~] is not present. Otherwise, the system put out a newline and halts documentation printing on the present topic, which can be resumed if the user types
moreat the terminal.
The other uses of the tilde character are of the following form.
~key[arg]Before launching into an explanation of how this works in detail, let us consider some small examples.
Here is a word that is code:
~c[function-name].Here is a phrase with an ``emphasized'' word, ``not'':
Do ~em[not] do that.Here is the same phrase, but where ``not'' receives stronger emphasis (presumably boldface in a printed version):
Do ~st[not] do that.Here is a passage that is set off as a display, in a fixed-width font:
~bv This passage has been set off as ``verbatim''. The present line starts just after a line break. Normally, printed text is formatted, but inside ~bv...~ev, line breaks are taken literally. ~evIn general, the idea is to provide a ``markup language'' that can be reasonably interpreted not only at the terminal (via
doc), but also via translators into other languages. In fact, translators have been written into Texinfo and HTML.
Let us turn to a more systematic consideration of how to mark text
in documentation strings using expressions of the form
~key[arg], which we will call ``doc-string tilde directives.''
The idea is that
key informs the documentation printer (which
could be the terminal, a hardcopy printer, or some hypertext tool)
about the ``style'' used to display
arg. The intention is that
each such printer should do the best it can. For example, we have
seen above that
~em[arg] tells the printer to emphasize
arg if possible, using an appropriate display to indicate
emphasis (italics, or perhaps surrounding
arg with some character
_, or ...). For another example, the directive for bold
~b[arg], says that printed text for
arg should be in
bold if possible, but if there is no bold font available (such as at
the terminal), then the argument should be printed in some other
reasonable manner (for example, as ordinary text). The
is case-insensitive; for example, you can use ~BV or ~Bv or ~bV in
place of ~bv.
Every form below may have any string as the argument (inside
[..]), as long as it does not contain a newline (more on that
below). However, when an argument does not make much sense to us,
we show it below as the empty string, e.g., ``
~- Print the equivalent of a dash ~b[arg] Print the argument in bold font, if available ~bid[arg] ``Begin implementation dependent'' -- Ignores argument at terminal. ~bf Begin formatted text (respecting spaces and line breaks), but in ordinary font (rather than, say, fixed-width font) if possible ~bq Begin quotation (indented text, if possible) ~bv Begin verbatim (print in fixed-width font, respecting spaces and line breaks) ~c[arg] Print arg as ``code'', such as in a fixed-width font ~ef End format; balances ~bf ~eid[arg] ``End implementation dependent'' -- Ignores argument at terminal. ~em[arg] Emphasize arg, perhaps using italics ~eq End quotation; balances ~bq ~ev End verbatim; balances ~bv ~i[arg] Print arg in italics font ~id[arg] ``Implementation dependent'' -- Ignores argument at terminal. ~il[arg] Print argument as is, but make it a link to another doc topic (for true hypertext environments). Note that the link argument must match the package name for the desired topic unless the package name is ``ACL2''. That is, to link to documentation on ``foo::topic'', one needs to use the full name for ``foo::topic'', including its package name. ~ilc[arg] Same as ~il[arg], except that arg should be printed as with ~c[arg] ~l[arg] Ordinary link to another doc topic; prints as ``See :DOC arg'' at the terminal (but also see ~pl below, which puts ``see'' in lower case) ~nl Print a newline ~par Paragraph mark, of no significance at the terminal (can be safely ignored; see also notes below) ~pl[arg] Parenthetical link (borrowing from Texinfo): same as ~l[arg], except that ``see'' is in lower case. This is typically used at other than the beginning of a sentence. ~sc[arg] Print arg in (small, if possible) capital letters ~st[arg] Strongly emphasize arg, perhaps using a bold font ~t[arg] Typewriter font; similar to ~c[arg], but leaves less doubt about the font that will be used. ~terminal[arg] Terminal only; arg is to be ignored except when reading documentation at the terminal, using :DOC. ~url[arg] Print arg as HTML hyperlink if possible (else print like
Style notes and further details
It is not a good idea to put doc-string tilde directives inside
~bv ... ~ev.
Do not nest doc-string tilde directives; that is, do not write
The ~c[~il[append] function ...but note that the ``equivalent'' expression
The ~ilc[append] function ...is fine. The following phrase is also acceptable:
~bfThis is ~em[formatted] text. ~efbecause the nesting is only conceptual, not literal.
We recommend that for displayed text,
should usually each be on lines by themselves. That way, printed
text may be less encumbered with excessive blank lines. Here is an
Here is some normal text. Now start a display: ~bv 2 + 2 = 4 ~ev And here is the end of that paragraph. Here is the start of the next paragraph.The analogous consideration applies to
~efas well as
You may ``quote'' characters inside the
arg part of
~key[arg], by preceding them with ~. This is, in fact, the
only legal way to use a newline character or a right bracket (])
inside the argument to a doc-string tilde directive.
Write your documentation strings without hyphens. Otherwise, you may find your text printed on paper (via TeX, for example) like this --
Here is a hyphe- nated word.even if what you had in mind was:
Here is a hyphe- nated word.When you want to use a dash (as opposed to a hyphen), consider using ~-, which is intended to be interpreted as a ``dash.'' For example:
This sentence ~- which is broken with dashes ~- is boring.would be written to the terminal (using
doc) by replacing
~-with two hyphen characters, but would presumably be printed on paper with a dash.
Be careful to balance the ``begin'' and ``end'' pairs, such as
~ev. Also, do not use two ``begin''
~bv) without an
intervening ``end'' directive. It is permissible (and perhaps this
is not surprising) to use the doc-string part separator
between such a begin-end pair.
Because of a bug in texinfo (as of this writing), you may wish to
avoid beginning a line with (any number of spaces followed by) the
- character or
The ``paragraph'' directive,
~par, is rarely if ever used.
There is a low-level capability, not presently documented, that
interprets two successive newlines as though they were
This is useful for the HTML driver. For further details, see the
authors of ACL2.
Emacs code is available for manipulating documentation strings that contain doc-string tilde-directives (for example, for doing a reasonable job filling such documentation strings). See the authors if you are interested.
We tend to use
~em[arg] for ``section headers,'' such as
``Style notes and further details'' above. We tend to use
~st[arg] for emphasis of words inside text. This division
seems to work well for our Texinfo driver. Note that
arg to be printed in upper-case at the terminal (using
arg to be printed at the
terminal as though
arg were not marked for emphasis.
Our Texinfo and HTML drivers both take advantage of capabilities for
indicating which characters need to be ``escaped,'' and how. Unless
you intend to write your own driver, you probably do not need to
know more about this issue; otherwise, contact the ACL2 authors. We
should probably mention, however, that Texinfo makes the following
requirement: when using
one of the special characters
}, you must
immediately follow this use with a period or comma. Also, the Emacs
``info'' documentation that we generate by using our Texinfo driver
has the property that in node names,
: has been replaced by
(because of quirks in info); so for example, the ``proof-checker''
s, is documented under
rather than under
We have tried to keep this markup language fairly simple; in
particular, there is no way to refer to a link by other than the
actual name. So for example, when we want to make
invisible link in ``code'' font, we write the following form, which
: should be in that font and then
both be in that font and be an invisible link.