Save-rendered
Saves the XDOC database into files for the acl2-doc browser
Also see save-rendered-event for a corresponding macro that
provides additional functionality.
General Form:
(save-rendered outfile
header
topic-list-name
error
write-acl2-doc-search-file
state)
where outfile is the pathname for the output file containing rendered
documentation, header is to be written to the top of
outfile (typically as a comment), and the value of topic-list-name
is a symbol that can be the first argument of defconst, hence of the
form *c*. The value of error should be t or nil to
indicate whether or not (respectively) to cause an error upon encountering a
syntax error in xdoc source (marked by "xdoc error"). When the value of
write-acl2-doc-search-file is not nil, then a file
"acl2-doc-search" is written, to be used for speeding up ACL2::ACL2-doc search commands.
Upon success, the call displayed above returns the error-triple (mv
nil (value-triple :ok) state); probably the value is unimportant except that
it allows an xdoc::save-rendered call to be placed inside
make-event, as displayed below.
For example, the following form may be found in community book
books/doc/top.lisp. Its evaluation creates the output file
books/system/doc/rendered-doc-combined.lsp". That file starts with a
comment from the string, *rendered-doc-combined-header*, then contains
(in-package "ACL2"), and concludes with a form (defconst
*ACL2+BOOKS-DOCUMENTATION* '<big-alist>), where <big-alist> is an alist
representing the XDOC database.
(make-event
(time$
(xdoc::save-rendered
(extend-pathname (cbd)
"../system/doc/rendered-doc-combined.lsp"
state)
*rendered-doc-combined-header*
'*acl2+books-documentation*
t ; cause error upon encountering xdoc error
state)))
The output file is typically used by the acl2-doc Emacs-based browser for
XDOC. See ACL2::ACL2-doc, specifically the discussion of custom
manuals, which explains that the filename argument of Emacs function
extend-acl2-doc-manual-alist is exactly the output file created by
xdoc::save-rendered.
