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 database.'' The database 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 database, 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 database under the symbol name we make a new entry in the section-name section of the database. 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 database 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 database 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.