		Search-engine friendly clone of the ACL2 documentation.

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)))))))))))