MARKUP

the markup language for ACL2 documentation strings 
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 :more processing when printing to the terminal. If the system is not doing :more processing, 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 :more at 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.
  ~ev[]
In 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 like _, or ...). For another example, the directive for bold font, ~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 key part 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., ``~bv[]'' rather than ``~bv[arg]''. 

~-[]      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 (for true
          hypertext environments)


~ilc[arg] Same as ~il[arg], except that arg should be printed as
          with ~c[arg]


~l[arg]   Ordinary link; 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.

Style notes and further details

It is not a good idea to put doc-string tilde directives inside verbatim environments, ~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: 
  ~bf[]This is
  ~em[formatted] text.
  ~ef[]
because the nesting is only conceptual, not literal.

We recommend that for displayed text, ~bv[] and ~ev[] should usually each be on lines by themselves. That way, printed text may be less encumbered with excessive blank lines. Here is an example. 

  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 ~bf[] and ~ef[] as well as ~bq[] and ~eq[].

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 ~bv[] and ~ev[]. Also, do not use two ``begin'' directives (~bf[], ~bq[], or ~bv[]) without an intervening ``end'' directive. It is permissible (and perhaps this is not surprising) to use the doc-string part separator ~/ while 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 ~par[]. 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 ~st[arg] causes arg to be printed in upper-case at the terminal (using :doc), while ~em[arg] causes 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 ~l[arg], where arg contains one of the special characters @, {, or }, 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'' simplification command, s, is documented under acl2-pc||s rather than under acl2-pc::s.

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 :doc an invisible link in ``code'' font, we write the following form, which indicates that : should be in that font and then doc should both be in that font and be an invisible link. 

  ~c[:]~ilc[doc]