• 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-input-processing

Generate an XDOC topic for the input processing that is part of the implementation of an event macro.

This macro accepts additional pieces of XDOC text, which are added at the end of the generated :long.

Macro: evmac-topic-input-processing

(defmacro xdoc::evmac-topic-input-processing
          (macro &rest additional)
 (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 "-INPUT-PROCESSING"))
   (parent-topic (add-suffix macro "-IMPLEMENTATION"))
   (short (concatenate 'string
                       "Input processing performed by "
                       macro-ref "."))
   (long
    (cons
     'xdoc::topstring
     (cons
      '(xdoc::p "See "
                (xdoc::seetopic "acl2::event-macro-input-processing"
                                "input processing")
                " for general background.")
      additional))))
  (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)))))))))))