• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
    • B*
    • Defunc
    • Fty
    • Apt
    • Std/util
    • Defdata
    • Defrstobj
    • Seq
    • Match-tree
    • Defrstobj
    • With-supporters
    • Def-partial-measure
    • Template-subst
    • Soft
    • Defthm-domain
    • Event-macros
      • Evmac-input-hints-p
      • Evmac-input-print-p
      • Event-macro-input-processing
      • Function-definedness
      • Event-macro-screen-printing
      • 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
        • Event-macro-xdoc-constructors-implementation-level
          • Xdoc::evmac-topic-implementation
          • Xdoc::evmac-topic-event-generation
          • Xdoc::evmac-topic-input-processing
          • Xdoc::evmac-topic-library-extensions
      • 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
  • Math
  • Testing-utilities

• Event-macro-xdoc-constructors-implementation-level

Xdoc::evmac-topic-library-extensions

Generate an XDOC topic for the library extensions that are part of the implementation of an event macro.

Macro: evmac-topic-library-extensions

(defmacro xdoc::evmac-topic-library-extensions (macro)
 (declare (xargs :guard (symbolp macro)))
 (b*
  ((macro-name (string-downcase (symbol-name macro)))
   (macro-ref (concatenate 'string
                           "@(tsee " macro-name ")"))
   (this-topic (add-suffix macro "-LIBRARY-EXTENSIONS"))
   (parent-topic (add-suffix macro "-IMPLEMENTATION"))
   (short (concatenate 'string
                       "Library extensions for "
                       macro-ref "."))
   (long
    (xdoc::topstring-p
     "These are used by, but more general than, "
     macro-ref
     ". Thus, they should be moved
                 to more general libraries eventually.")))
  (cons
   'defxdoc+
   (cons
    this-topic
    (cons
     ':parents
     (cons
      (cons parent-topic 'nil)
      (cons
       ':short
       (cons
         short
         (cons ':long
               (cons long
                     '(:order-subtopics t
                                        :default-parent t)))))))))))