		Search-engine friendly clone of the ACL2 documentation.

Output-files

Output-files-implementation

Implementation of output-files.

This also implements the programmatic interface output-files-prog. The flag progp, passed to some of the implementation functions below, says whether the programmatic interface has been called.

Subtopics

Output-files-process-inputs: Process the inputs.
Output-files-process-const/arg: Process the :const or arg input.
Output-files-process-printer-options: Process the :printer-options input.
Output-files-gen-files: Generate the files.
Output-files-fn: Event expansion of output-files from the inputs.
Output-files-process-path: Process the :path input.
Output-files-process-inputs-and-gen-files: Process the inputs and generate the files.
*output-files-printer-options*: Keyword options accepted in the :printer-options of output-files.
*output-files-allowed-options*: Keyword options accepted by output-files.
Output-files-definition: Definition of the output-files macro.