Construct the redundancy section of the user documentation of an event macro.
This assumes an event macro with a
Since this documentation is part of the XDOC topic
whose name is the name of the macro,
the
Macro:
(defmacro xdoc::evmac-section-redundancy (macro) (declare (xargs :guard (symbolp macro))) (b* ((macro-name (string-downcase (symbol-name macro))) (macro-ref (concatenate 'string "@('" macro-name "')"))) (cons 'xdoc::section (cons 'xdoc::*evmac-section-redundancy-title* (cons (cons 'xdoc::p (cons (cons 'concatenate (cons ''string (cons '"A call of " (cons macro-ref (cons '" is redundant if and only if it is identical to a previous successful call of " (cons macro-ref '(" whose @(':show-only') input is not @('t'), except that the two calls may differ in their @(':print') and @(':show-only') inputs. These inputs do not affect the generated events, and thus they are ignored for the purpose of redundancy."))))))) 'nil)) (cons (cons 'xdoc::p (cons (cons 'concatenate (cons ''string (cons '"A call of " (cons macro-ref '(" whose @(':show-only') input is @('t') does not generate any event. Thus, no successive call may be redundant with such a call."))))) 'nil)) 'nil))))))