Xdoc::evmac-appcond
Construct an applicability condition description
in the user documentation of an event macro.
This generates an xdoc::desc.
The name input must be a string
that names the applicability condition.
The main input must be an XDOC tree
that contains the main description of the applicability condition,
consisting of explanatory natural language
and formal code for the formula(s).
The design-notes and design-notes-appcond inputs
must be either both present or both absent.
If present, they must be both XDOC trees:
the first one references the design notes of the event macro
(which usually includes a link to the design notes);
the second one provides the name of the applicability condition
(usually some mathematical notation) used in the design notes.
If these two inputs are present,
the generated XDOC includes text
relating the applicability condition to the design notes.
If the presence input is present,
it must be an XDOC tree.
In this case,
the generated XDOC includes text
explaining that the applicability condition is present
under the condition described by the presence input.
Macro: evmac-appcond
(defmacro xdoc::evmac-appcond (name main &key design-notes
design-notes-appcond presence)
(declare (xargs :guard (stringp name)))
(cons
'xdoc::desc
(cons
(concatenate 'string "@('" name "')")
(cons
main
(append
(and
design-notes design-notes-appcond
(cons (cons 'xdoc::p
(cons '"This corresponds to "
(cons design-notes-appcond
(cons '" in the "
(cons design-notes '("."))))))
'nil))
(and
presence
(cons
(cons
'xdoc::p
(cons
'"This applicability condition is present if and only if "
(cons presence '("."))))
'nil)))))))
