• 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
        • Missing-parents
        • Archive-xdoc
        • Xdoc-extend
        • 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
      • Projects
      • Debugging
      • Std
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Testing-utilities
      • Math
    • Xdoc

    Defxdoc-raw

    Add documentation in raw mode.

    Defxdoc-raw allows you to document raw-lisp code with XDOC. It isn't possible to do this with the ordinary defxdoc command because defxdoc is a macro that expands to a make-event, and make-event is not permitted in raw Lisp.

    Defxdoc-raw is not available just by including xdoc/top, because it requires a ttag. So, to use it you will need:

    (include-book "xdoc/defxdoc-raw" :dir :system)

    Defxdoc-raw takes the same arguments as defxdoc, but adds its documentation to a Lisp variable rather than to the XDOC table. Note that the :xdoc and save commands already know about this table, so to the end-user, documentation added by defxdoc-raw is not any different than documentation added by defxdoc.