|
|
|---|
|
|
|
|---|
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-print (macro &key additional) (declare (xargs :guard (symbolp macro))) (b* ((macro-name (string-downcase (symbol-name macro))) (macro-ref (concatenate 'string "@('" macro-name "')"))) (cons 'xdoc::desc (cons '"@(':print') — default @(':result')" (cons '(xdoc::p "Specifies what is printed on the screen (see " (xdoc::seetopic "acl2::event-macro-screen-printing" "screen printing") ").") (cons '(xdoc::p "It must be one of the following:") (cons (cons 'xdoc::ul (cons '(xdoc::li "@('nil'), to print nothing (not even error output).") (cons '(xdoc::li "@(':error'), to print only error output (if any).") (cons (cons 'xdoc::li (cons '"@(':result'), to print, besides any error output, also the " (cons '(xdoc::seetopic "acl2::event-macro-results" "results") (cons '" of " (cons macro-ref '(". This is the default value of the @(':print') input.")))))) (cons (cons 'xdoc::li (cons '"@(':info'), to print, besides any error output and the results, also some additional information about the internal operations of " (cons macro-ref '(".")))) '((xdoc::li "@(':all'), to print, besides any error output, the results, and the additional information, also ACL2's output in response to all the submitted events."))))))) (cons (cons 'xdoc::p (cons '"If the call of " (cons macro-ref '(" is redundant, an indication to that effect is printed on the screen, unless @(':print') is @('nil').")))) additional))))))))