• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
      • B*
      • Defunc
      • Fty
      • Std/util
      • Apt
      • Defdata
      • Defrstobj
      • Seq
      • Match-tree
      • Defrstobj
      • With-supporters
      • Def-partial-measure
      • Template-subst
      • Soft
      • Defthm-domain
      • Event-macros
        • Evmac-input-hints-p
        • Function-definedness
        • Event-macro-input-processing
        • Event-macro-screen-printing
        • Evmac-input-print-p
        • Make-event-terse
        • Event-macro-applicability-conditions
        • Event-macro-results
        • Template-generators
        • Event-macro-event-generators
        • Event-macro-proof-preparation
        • Try-event
        • Restore-output?
        • Restore-output
        • Fail-event
        • Cw-event
        • Event-macro-xdoc-constructors
          • Event-macro-xdoc-constructors-user-level
            • Xdoc::evmac-desc-function/lambda/macro
            • Xdoc::evmac-desc-term
            • Xdoc::evmac-topic-design-notes
            • Xdoc::evmac-appcond
            • Xdoc::evmac-desc-input-name
            • Xdoc::evmac-section-redundancy
            • Xdoc::evmac-input-show-only
            • Xdoc::evmac-input-print
            • Xdoc::evmac-desc-input-enable-t/nil
            • Xdoc::evmac-section-appconds
            • Xdoc::evmac-input-hints
            • Xdoc::evmac-subsubsubsection
            • Xdoc::evmac-subsubsection
            • Xdoc::evmac-subsection
            • Xdoc::evmac-section
            • Xdoc::evmac-section-intro
            • Xdoc::evmac-section-inputs
            • Xdoc::evmac-section-generated
            • Xdoc::evmac-section-form
          • Event-macro-xdoc-constructors-implementation-level
        • Event-macro-intro-macros
      • Def-universal-equiv
      • Def-saved-obligs
      • With-supporters-after
      • Definec
      • Sig
      • Outer-local
      • Data-structures
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Testing-utilities
    • Math
  • Event-macro-xdoc-constructors

Event-macro-xdoc-constructors-user-level

Utilities to construct XDOC strings to document event macros at the user level.

The xdoc::evmac-section-... utilities construct level-3 sections. Some are relatively thin wrappers, which precede their arguments (which must be zero or more pieces of XDOC text) with specific level-3 headings. Other utilities provide more automation.

The xdoc::evmac-input-... utilities construct descriptions of inputs that are expected to be common to multiple event macros. Each such utility includes zero or more parameters to customize the description, as well as zero or more additional pieces of XDOC text (e.g. paragraphs) that are appended after the automatically generated XDOC text.

Subtopics

Xdoc::evmac-desc-function/lambda/macro
Construct a common description text for an input that must be a function name or a lambda expression or a macro name.
Xdoc::evmac-desc-term
Construct a common description text for an input that must be a term.
Xdoc::evmac-topic-design-notes
Generate an XDOC topic for the design notes of an event macro.
Xdoc::evmac-appcond
Construct an applicability condition description in the user documentation of an event macro.
Xdoc::evmac-desc-input-name
Construct a description of a :...-name input for the user documentation of an event macro.
Xdoc::evmac-section-redundancy
Construct the redundancy section of the user documentation of an event macro.
Xdoc::evmac-input-show-only
Construct a description of the :show-only input for the user documentation of an event macro.
Xdoc::evmac-input-print
Construct a description of the :print input for the user documentation of an event macro.
Xdoc::evmac-desc-input-enable-t/nil
Construct a description of a :...-enable input for the user documentation of an event macro.
Xdoc::evmac-section-appconds
Construct the applicability conditions section of the user documentation of an event macro.
Xdoc::evmac-input-hints
Construct a description of the :hints input for the user documentation of an event macro.
Xdoc::evmac-subsubsubsection
Construct a subsubsubsection of the user documentation of an event macro.
Xdoc::evmac-subsubsection
Construct a subsubsection of the user documentation of an event macro.
Xdoc::evmac-subsection
Construct a subsection of the user documentation of an event macro.
Xdoc::evmac-section
Construct a section of the user documentation of an event macro.
Xdoc::evmac-section-intro
Construct the introduction section of the user documentation of an event macro.
Xdoc::evmac-section-inputs
Construct the inputs section of the user documentation of an event macro.
Xdoc::evmac-section-generated
Construct the generated events section of the user documentation of an event macro.
Xdoc::evmac-section-form
Construct the general form section of the user documentation of an event macro.