Event that invokes save-rendered, supporting extra functionality
See save-rendered for relevant background.
script-file script-args timep write-acl2-doc-search-file)
where the four required arguments correspond to the same arguments of
save-rendered. Although save-rendered and
save-rendered-event have similar effects — indeed,
save-rendered-event invokes save-rendered with the same first four
arguments — save-rendered-event is a macro that generates an event
form (using make-event) that can be placed in a book. All arguments
are evaluated. The keyword arguments of save-rendered-event provide
additional functionality, as follows.
Suppose :script-file is supplied with a non-nil value. Then
there must be an active trust tag (see defttag. The value of
:script-file should be a string that names a file to be executed as a
shell command, using sys-call. The argument list of that command is
provided by the value of :script-args. For an example, see the call of
xdoc::save-rendered-event in community book doc/top.lisp.
If :timep is non-nil then the entire computation will be wrapped
in a call of time$.
The value of keyword option :write-acl2-doc-search-file, which is
nil by default, is passed directly to the corresponding parameter of