		Search-engine friendly clone of the ACL2 documentation.

Event-macro-xdoc-constructors-user-level

Xdoc::evmac-input-show-only

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

Since this documentation is part of the XDOC topic whose name is the name of the macro, the macro-ref variable is not a link.

Macro: evmac-input-show-only

(defmacro xdoc::evmac-input-show-only (macro &key additional)
 (declare (xargs :guard (symbolp macro)))
 (b* ((macro-name (string-downcase (symbol-name macro)))
      (macro-ref (concatenate 'string
                              "@('" macro-name "')"))
      (redundancy-ref
           (concatenate 'string
                        "`"
                        xdoc::*evmac-section-redundancy-title*
                        "' section")))
  (cons
   'xdoc::desc
   (cons
    '"@(':show-only') &mdash; default @('nil')"
    (cons
     (cons
      'xdoc::p
      (cons
       (cons
           'concatenate
           (cons ''string
                 (cons '"Determines whether the event expansion of "
                       (cons macro-ref
                             '(" is submitted to ACL2 or just printed on the screen:")))))
       'nil))
     (cons
      (cons
       'xdoc::ul
       (cons
        '(xdoc::li "@('nil'), to submit it.")
        (cons
         (cons
          'xdoc::li
          (cons
           (cons
            'concatenate
            (cons
             ''string
             (cons
              '"@('t'), to just print it.
          In this case:
          the event expansion is printed even if @(':print') is @('nil')
          (because the user has explicitly asked to show the event expansion);
          the resulting events are not re-printed separately
          (other than their appearance in the printed event expansion)
          even if @(':print') is @(':result') or @(':info') or @(':all');
          no ACL2 output is printed for the event expansion
          even if @(':print') is @(':all')
          (because the event expansion is not submitted).
          If the call of "
              (cons
                macro-ref
                (cons '" is redundant
          (as defined in the "
                      (cons redundancy-ref
                            '("), the event expansion generated by the existing call
          is printed.")))))))
           'nil))
         'nil)))
      additional))))))