		Search-engine friendly clone of the ACL2 documentation.

Xdoc

Archive-matching-topics

An event that saves documentation from certain events, filtered by customizable criteria.

This event has a similar purpose to that of archive-xdoc. However, instead of acting on the new xdoc topics that are created by some set of local events, it acts on all existing topics that fit some matching criterion.

Usage: <term> must be a term that uses a variable named X (in any package); it may also use acl2::world and acl2::state. The following form preprocesses all existing xdoc topics for which term returns true (non-NIL) when the topic is bound to X and the current acl2 world and state are bound to world and state, respectively.

(archive-matching-topics <term>)

Thus the following could be put in a book that, when included, loads all the documentation from std/strings but does not load the actual functions and events from there:

(include-book "xdoc/archive-matching-topics" :dir :system)
(local (include-book "std/strings/top" :dir :system))

(archive-matching-topics (str::strprefixp "std/strings/" (cdr (assoc :from x))))

The topics that are archived by this event may be ones that were process assumes that at the point of saving the xdoc, the definitions referenced in these preprocessor forms exist and the @(`...`) forms can be evaluated. If the documentation loaded in the archive-xdoc form references definitions that aren't loaded, then the preprocessing will produce xdoc-errors and leave notes behind in the documentation saying that those definitions couldn't be found.