Construct a description of the
Since this documentation is part of the XDOC topic
whose name is the name of the macro,
the
Macro:
(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') — 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))))))