• Top
    • Documentation
      • Xdoc
        • Undocumented
        • Save
        • Defsection
        • Markup
        • Preprocessor
        • Emacs-links
        • Defxdoc
        • Katex-integration
        • Constructors
        • Entities
        • Save-rendered
        • Add-resource-directory
        • Defxdoc+
        • Testing
        • Order-subtopics
        • Save-rendered-event
          • Archive-matching-topics
          • Archive-xdoc
          • Xdoc-extend
          • Missing-parents
          • Set-default-parents
          • Defpointer
          • Defxdoc-raw
          • Xdoc-tests
          • Xdoc-prepend
          • Defsection-progn
          • Gen-xdoc-for-file
        • ACL2-doc
        • Pointers
        • Doc
        • Documentation-copyright
        • Args
        • ACL2-doc-summary
        • Finding-documentation
        • Broken-link
      • Books
      • Recursion-and-induction
      • Boolean-reasoning
      • Debugging
      • Projects
      • Std
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Testing-utilities
      • Math
    • Xdoc

    Save-rendered-event

    Event that invokes save-rendered, supporting extra functionality

    See save-rendered for relevant background.

    General Form:
    
    (save-rendered-event outfile
                         header
                         topic-list-name
                         error
                         &key
                         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 save-rendered.