Major Section: EVENTS
Examples: (defdoc interp-section ":Doc-Section ...") General Form: (defdoc name doc-string)where
name is a symbol or string to be documented and
doc-string is a documentation string (see doc-string). This
event adds the documentation string for symbol name to the
:doc database. It may also be used to change the documentation
for name if name already has documentation. The difference
between this event and deflabel is that, unlike deflabel (but
like table), it does not mark the current history with the
name. But like deflabel, defdoc events are never
considered redundant (see redundant-events).See deflabel for a means of attaching a documentation string to
a name that marks the current history with that name. We now
elaborate further on how defdoc may be useful in place of deflabel.
It is usually sufficient to use deflabel when you might be tempted
to use defdoc. However, unlike deflabel, defdoc does not mark
the current history with name. Thus, defdoc is useful for
introducing the documentation for a defun or deftheory event,
for example, several events before the function or theory is
actually defined.
For example, suppose you want to define a theory (using deftheory).
You need to prove the lemmas in that theory before executing the
deftheory event. However, it is quite natural to define a
:Doc-Section (see doc-string) whose name is the name of the
theory to be defined, and put the documentation for that theory's
lemmas into that :Doc-Section. Defdoc is ideal for this purpose,
since it can be used to introduce the :Doc-Section, followed by the
lemmas referring to that :Doc-Section, and finally concluded with a
deftheory event of the same name. If deflabel were used
instead of defdoc, for example, then the deftheory event would
be disallowed because the name is already in use by the deflabel
event.
We also imagine that some users will want to use defdoc to insert
the documentation for a function under development. This defdoc
event would be followed by definitions of all the subroutines of
that function, followed in turn by the function definition itself.
Any time defdoc is used to attach documentation to an
already-documented name, the name must not be attached to a new
:Doc-Section. We make this requirement as a way of avoiding
loops in the documentation tree. When documentation is redefined, a
warning will be printed to the terminal.
