		Search-engine friendly clone of the ACL2 documentation.

Xdoc

Xdoc-extend

Extend an existing XDOC topic with additional content.

Basic example:

(defxdoc foo
  :short "Example of xdoc-extend."
  :long "<p>Foo is very important.</p>")

(xdoc::xdoc-extend foo
  "<p>Note: you can't use Foo with Bar.</p>")

is roughly equivalent to just writing:

(defxdoc foo
  :short "Example of xdoc-extend."
  :long "<p>Foo is very important.</p>
          <p>Note: you can't use Foo with Bar.</p>")

(xdoc-extend name long) requires that name is an existing XDOC topic, e.g., it may have been introduced with defxdoc, defsection, or similar. We just look up that topic and extend its :long string by appending the new long fragment to it.

This mechanism is barbaric and fragile. For instance:

You can't put the new content anywhere except at the end of the current long string. (But see xdoc-prepend if you want to extend the beginning of a topic).
If you extend a topic several times in different books, the resulting text may differ depending on the particular include-book order that happens to be used.

Nevertheless, judiciously used, it can be a useful tool for connecting together related content that must be kept in separate files, e.g., for bootstrapping or other reasons.