		Search-engine friendly clone of the ACL2 documentation.

Xdoc

Set-default-parents

Set up default parents to use for xdoc.

When documenting a book of inter-related functions, you may sometimes wish to use the same :parents across many defxdoc or defsection commands. This can sometimes get tedious.

The macro (set-default-parents &rest parents) can be used to set up a default list of parent topics to be automatically used by commands such as defxdoc and defsection.

Basic Example:

(local (set-default-parents fox-p))

(defxdoc make-fox           ;; use default :parents, (fox-p)
  :short ...
  :long ...)

(defsection feed-fox        ;; use default :parents, (fox-p)
  :short ...
  :long ...)

(defsection chase-mouse     ;; use explicit :parents, (fox-p mouse-p)
  :parents (fox-p mouse-p)
  :short ...
  :long ...)

(local (set-default-parents fox-p hawk-p))

(defsection bother-hawk     ;; use default :parents, (fox-p hawk-p)
  :short ...
  :long ...)

(local (set-default-parents nil))

(defxdoc zebra-p            ;; use default :parents, nil
  :short ...
  :long ...)

Note that set-default-parents is just a macro that expands to a table event. It's good practice to only locally set the default parents—otherwise the default parents can "leak" from your book and lead you to inadvertently set the parents of other, unrelated topics.