*TERMINAL-MARKUP-TABLE*

Major Section:  DOCUMENTATION

The value of the ACL2 constant *terminal-markup-table* is an association list pairing markup keys with strings, to be used for printing to the terminal. See markup for a description of the ACL2 markup language.

The entries in *terminal-markup-table* are of the form

(key . fmt-string)

It is possible to implement tools in ACL2 for printing documentation to other than the terminal. In fact, such tools exist for Texinfo and for HTML. For now, discussion of this capability is beyond the scope of the present topic.

ARGS

Major Section:  DOCUMENTATION

Example:
:args assoc-eq

Args takes one argument, a symbol which must be the name of a function or macro, and prints out the formal parameters, the guard expression, the output signature, the deduced type, the constraint (if any), and whether documentation about the symbol is available via :doc. The output signature is either & indicating that the function returns one value; state, indicating that it returns a state, or an expression (mv & & ... state ... &) indicating how many multiple values it returns and which if any is a state.

DOC

Major Section:  DOCUMENTATION

NOTE: The :doc command only makes sense at the terminal. Furthermore it only works at the terminal when a ``full-size'' image has been built. Most users will probably access the ACL2 documentation in other ways, as explained in the file "doc/README" that comes with the ACL2 distribution.

Examples:
ACL2 !>:doc DEFTHM          ; print documentation of DEFTHM
ACL2 !>:doc logical-name    ; print documentation of LOGICAL-NAME
ACL2 !>:doc "MY-PKG"      ; print documentation of "MY-PKG"


Related Topics:
:more                      ; continues last :doc or :more-doc text
:more-doc name             ; prints more documentation for name
:docs **                   ; lists all documented symbols
:docs "compil"             ; documented symbols apropos "compil"
:DOC documentation         ; describes how documentation works

General Form:
ACL2>:doc logical-name

For a general discussion of our treatment of documentation strings, see documentation.

This is the first cut at online documentation. Users can be particularly helpful by sending mail on the inadequacies of the system. Address it just to Moore and put Documentation in the subject line. There are several things that trouble me about what I've done here.

First, many concepts aren't documented. Ultimately, I'd like to . document (a) every CLTL primitive (e.g., case and coerce) and (b) every ACL2 extension (e.g., aref1 and getprop). But so far I have focussed on documenting (c) the ACL2 system primitives (e.g., defthm and what hints look like). My priorities are (c), then (b), and then (a), following the philosophy that the most unstable features should get online documentation in these early releases. Having gotten the basic documentation in place, I'll document new things as they are added, and in response to your pleas I'll try to add documentation to old things that are widely regarded as important.

Second, I worry that the existing documentation is unhelpful because it provides too much or too little detail, or it provides the detail too far away from where it is needed. Please be on the lookout for this. Did you get what you needed when you appealed to :doc or :more-doc? If not, what was it you needed? Would more cross-references help? Did you get lost in maze of cross-references?

DOC!

Major Section:  DOCUMENTATION

NOTE: The :doc! command only makes sense at the terminal.

Examples:
ACL2 !>:doc! defthm
ACL2 !>:doc! certificate

This command is like :doc name followed by :more!. It prints all the documentation of name.

DOC-STRING

Major Section:  DOCUMENTATION

Examples:
":Doc-Section name
one-liner~/notes~/details"


":Doc-Section name
one-liner~/
notes~/
details~/
:cite old-name1
:cited-by old-name2"

Documentation strings not beginning with ``:Doc-Section'' (case is irrelevant) are ignored. See markup for how to supply formatting information (such as fonts and displayed text) in documentation strings.

ACL2 attaches special importance to documentation strings beginning with the header ``:Doc-Section'' (or any variant thereof obtained by changing case). Any documentation string that does not begin with such a header is considered unformatted and is ignored. For the rest of this discussion, we use the phrase ``documentation string'' as though it read ``formatted documentation string.''

Documentation strings are always processed in the context of some symbol, name, being defined. (Indeed, if an event defines no symbol, e.g., verify-guards or in-theory, then it is not permitted to have a formatted documentation string.) The string will be associated with name in the ``documentation data base.'' The data base is divided into ``sections'' and each section is named by a symbol. Among the sections are events, documentation, history, other, and miscellaneous. A complete list of the sections may be obtained by typing :docs * at the terminal. You can create new sections. The main purpose of sections is simply to partition the large set of names into smaller subsets whose contents can be enumerated separately. The idea is that the user may remember (or recognize) the relevant section name and then read its contents to find interesting items.

Within a section are ``documentation tuples'' which associate with each documented name its documentation string and a list of related documented names, called the ``related names'' of the name. When :doc prints the documentation for name, it always lists the related names.

When a formatted documentation string is submitted with the defining event of some name, the section name and an initial set of related names are parsed from the string. In addition, the formatted string contains various ``levels'' of detail that are printed out at different times. Finally, it is possible for a string to cause the newly documented name to be added to the related names of any previously documented name. Thus, as new names are introduced they can be grouped with old ones.

The general form of an ACL2 formatted documentation string is

":DOC-SECTION <section-name>
  <one-liner>~/
  <notes>~/
  <details>~/
  :CITE <n1>
  ...
  :CITE <nn>
  :CITED-BY <m1>
  ...
  :CITED-BY <mm>"

A formatted documentation string has five parts: the header and section-name (terminating in the first #\Newline), the <one-liner>, <notes>, and <details> (each terminating in a tilde-slash (``~/'') pair), and a citation part. These five parts are parsed into six components. <section-name> is read as the name of a symbol, section-name. <one-liner>, <notes>, and <details> are arbitrary sequences of characters (ignoring initial white space and not including the tilde-slash pairs which terminate them). The <ni> are read as symbols and assembled into a list called the ``cite'' symbols. The <mi> are read as symbols and assembled into a list called the ``cited-by'' symbols. See the warning below regarding the hackish nature of our symbol reader.

Section-name must either be a previously documented symbol or else be name, the symbol being documented. To open a new section of the data base, named section-name, you should define the logical name section-name (as by deflabel or any other event; also see defdoc) and attach to it a documentation string for section section-name. You might wish to print out the documentation string we use for some of our section names, e.g., (get-doc-string 'events state). By forcing section names to be documented symbols, we permit sections themselves to have one line descriptions and discussions, presented by the standard documentation facilities like the facilities :doc and :more-doc that may be used at the terminal.

Each of the ni's and mi's must be previously documented symbols.

Both <one-liner> and <details> must be non-empty, i.e., must contain some non-whitespace characters. <notes> may be empty. The :cites and :cited-bys pairs may be intermingled and may be separated by either newlines or spaces. The citation part may be empty. When the citation part is empty, the tilde-slash pair terminating the <details> part may be omitted. Thus, the simplest form of a formatted documentation string is:

":Doc-Section <section-name>
 <one-liner>~/~/
 <details>"

However, we find that when documentation is printed flush against the left margin it is difficult to distinguish the documentation text from previous output. We therefore prefix each line we print by a special pad of characters. By default, this pad is ``| '' so that documentation text has a vertical bar running down the left margin. But the pad is just the value of the global variable doc-prefix and you may assign it any string you wish.

To add such a string to the data base under the symbol name we make a new entry in the section-name section of the data base. The entry associates name with the string and uses the string's cites list as the initial value of the related names field. In addition, we add name to the related names field of each of the names listed in the string's cited-by list. We also add name to the related names field of its section-name. Observe that the cites list in a string is only the initial value of the related names of the names. Future documentation strings may add to it via :cited-by or :doc-section. Indeed, this is generally the case. We discuss this further below.

When a brief description of name is required (as by :docs **), name and <one-liner> are printed. <one-liner> is usually printed starting in column 15 (however see print-doc-start-column). Despite its name, <one-liner> need not be one line. It usually is one line, however.

When you type :doc name at the terminal, the first response will be to print name and <one-liner>. Then :doc prints <notes>, if any. Then, if name is the name of a section, it prints the <one-liner>s for each of its related names. For example, try :doc events. If name is not a section name but does have some related names, they are merely listed but not explained. Try :doc theory-functions. :more-doc name prints <details>.

Our style is to let each new concept add itself to the related names of old concepts. To do otherwise increases the chances that documentation gets outdated because one often forgets to update supposedly complete lists of the relevant topics when new topics are invented. For example, :doc theory-functions lists each available theory function. But get-doc-string of 'theory-functions just shows a few examples and has an empty cites list. From where do we get the names of the theory functions listed by :doc? The answer is that each theory function has its own documentation string and those strings each specify :cited-by theory-functions. See for example get-doc-string of 'union-theories. So by the time the entire system is assembled, the related names of 'theory-functions contains all the (documented) theory functions. This makes it easy to add new theory functions without changing the general discussion in 'theory-functions.

When an event or command form is printed, as by :pe or :pc, that contains a formatted documentation string, we do not print the actual documentation string (since they are usually large and distracting). Instead we print the string:

  "Documentation available via :doc"

Warning on Reading Symbols from Strings: When we read a symbol, such as the section-symbol, from a documentation string, we use a quick and dirty imitation of the much more powerful CLTL read program. In particular, we scan past any whitespace, collect all the characters we see until we get to more whitespace or the end of the string, convert the characters to upper case, make a string out of them, and intern that string. Thus, if you typed ":Doc-Section 123 ..." we would read the 123 as the symbol |123|. Observe that special characters, such as parentheses and escape characters, are not afforded their usual reverence by our hack. Furthermore, the question arises: in which package do we intern the symbol? The answer is, usually, the package containing the name being defined. I.e., if you are documenting my-pkg::name and you attach a documentation string that begins ":Doc-Section: Machines ..." then the section-symbol will be my-pkg::machines. We recognize two special cases. If the first character read is a colon, we use the keyword package. If the first five characters read are acl2:: then we intern in the "ACL2" package. Our own section names, e.g., events, are in the "ACL2" package.

In a related area, when you ask for the documentation of a name, e.g., when you type :doc name at the terminal, that name is read with the full ACL2 reader, not the hack just described. That name is read into the current package. Thus, if you are operating in-package "MY-PKG" and type :doc events, what is read is my-pkg::events. The data base may not contain an entry for this symbol. Before reporting that no documentation exists, we try acl2::events.

One last note: defpkg permits a formatted documentation string, which is associated in the data base with the name of the package. But the name of the package is a string, not a symbol. It is permitted to access the documentation of a string (i.e., package name). But there are no facilities for getting such a stringp name into the related names of another name nor of making such stringp names be section names. That is because we always read symbols from strings and never read strings from strings. I.e., if you did write "Doc-Section \"MY-PKG\" ..." it would read in as a weird symbol.

DOCS

Major Section:  DOCUMENTATION

NOTE: The :docs command only makes sense at the terminal.

Examples:
ACL2 !>:docs *           ; lists documentation sections
ACL2 !>:docs **          ; lists all documented topics within all sections
ACL2 !>:docs events      ; lists all topics in section EVENTS
ACL2 !>:docs "compil"    ; lists topics ``apropos''

The data base of formatted documentation strings is structured into sections. Within a section are topics. Each topic has a one-liner, some notes, and some detailed discussions. The :docs command provides a view of the entire data base.

:docs takes one argument, as described below:

arg               effect


*                 list all section headings in the data base
**                list all section headings and all topics within
                  each section
name              list all topics in the section named name (where
                  name is some symbol other than * and **).  This
                  is always the same as :doc name.
pattern           list all topics whose :doc or :more-doc text
                  mentions the string pattern.  For purposes of this
                  string matching we ignore distinctions of case and
                  the amount and kind (but not presence) of white
                  space.  We also treat hyphen as whitespace.

HELP

Major Section:  DOCUMENTATION

Example:
ACL2 !>:help

See lp for general information about the top-level command environment for ACL2.

MARKUP

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.

  ~key[arg]

Here is a word that is code:

  ~c[function-name].

  Do ~em[not] do that.

  Do ~st[not] do that.

  ~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[]

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

  The ~ilc[append] function ...

  ~bf[]This is
  ~em[formatted] text.
  ~ef[]

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.

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.

  Here is a hyphe-
  nated word.

  This sentence ~-[] which is broken with dashes ~-[] is boring.

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]

MORE

Major Section:  DOCUMENTATION

NOTE: The command :more only makes sense at the terminal.

Example:
ACL2 !>:more

When you type :doc name, for some documented name, the system responds by typing the one-liner and the notes sections of the documentation for name. It then types ``(cont'd)'' which stands for ``continued''. If you then type

ACL2 !>:more

Similarly, if you have typed :more-doc name, the system will print the first ``block'' of the details section and then print ``(cont'd)''. Typing :more at that point will cause the next block of the details section to be printed. Eventually :more will conclude by printing ``*-'' which is the indicator that the text has been exhausted.

What is a ``block'' of text? :More looks for the end of a paragraph (two adjacent newlines) after printing n lines. If it doesn't find one before it has printed k lines, it just stops there. N and k here are the values of the two state global variables 'more-doc-min-lines and 'more-doc-max-lines. You may use @ and assign to inspect and set these variables, e.g., (@ more-doc-max-lines) will return the current maximum number of lines printed by :more and (assign more-doc-max-lines 19) will set it to 19. On terminals having only 24 lines, we find min and max settings of 12 and 19 the most pleasant.

If you want :more to print all of the details instead of feeding them to you one block at a time, type :more! instead.