		Search-engine friendly clone of the ACL2 documentation.

Event-macro-xdoc-constructors-user-level

Xdoc::evmac-desc-input-name

Construct a description of a :...-name input for the user documentation of an event macro.

This is for an input to determine the name of an entity (e.g. a function) generated by the event macro.

The ... in :...-name is passed as the prefix argument of this macro.

A description of the entitty whose name is being determined is passed as the desc argument of this macro.

The auto-desc argument of this macro describes the name used when the :...-name input is :auto.

An XDOC tree of additional text can be passed as the additional argument of this macro.

The name-rest argument of this macro is the name that the generated documentation says that will be used as the name of the entity in the rest of the documentation page.

Macro: evmac-desc-input-name

(defmacro xdoc::evmac-desc-input-name
          (prefix &key
                  desc auto-desc additional name-rest)
 (declare (xargs :guard (and (stringp prefix)
                             (stringp desc)
                             (stringp auto-desc)
                             (stringp name-rest))))
 (cons
  'xdoc::desc
  (cons
   (concatenate 'string
                "@(':" prefix
                "-name') &mdash; default @(':auto')")
   (cons
    (cons 'xdoc::p
          (cons '"Determines the name of "
                (cons desc '("."))))
    (cons
     '(xdoc::p "It must be one of the following:")
     (cons
      (cons
       'xdoc::ul
       (cons (cons 'xdoc::li
                   (cons '"@(':auto'), to use "
                         (cons auto-desc '("."))))
             '((xdoc::li "Any other symbol, to use as the name."))))
      (append
       (and additional (list additional))
       (cons
        (cons
         'xdoc::p
         (cons
            '"In the rest of this documentation page,
      let @('"
            (cons name-rest '("') be this name."))))
        'nil))))))))