Generate an XDOC topic for the design notes of an event macro.
This utility takes the following arguments:
Macro:
(defmacro xdoc::evmac-topic-design-notes (macro notes-ref &key additional-parents correspondences additional-doc) (declare (xargs :guard (and (symbolp macro) (stringp notes-ref) (symbol-listp additional-parents)))) (b* ((macro-name (string-downcase (symbol-name macro))) (macro-ref (concatenate 'string "@(tsee " macro-name ")")) (this-topic (add-suffix macro "-DESIGN")) (parents (cons macro additional-parents)) (short (concatenate 'string "Design notes for " macro-ref ".")) (long (cons 'xdoc::topstring (cons (cons 'xdoc::p (cons '"The design of " (cons macro-ref (cons '" is described in " (cons (cons 'xdoc::a (cons ':href (cons notes-ref '("these notes")))) '(", which use " (xdoc::a :href "res/kestrel-design-notes/notation.pdf" "this notation") ".")))))) (append (and correspondences (cons '(xdoc::p "The correspondence between the design notes and the user documentation is the following:") (cons (cons 'xdoc::ul-fn (cons 'nil (cons (cons 'xdoc::evmac-topic-design-notes-make-bullets (cons (cons 'list correspondences) 'nil)) 'nil))) 'nil))) additional-doc))))) (cons 'defxdoc (cons this-topic (cons ':parents (cons parents (cons ':short (cons short (cons ':long (cons long 'nil))))))))))
Function:
(defun xdoc::evmac-topic-design-notes-make-bullets (correspondences) (declare (xargs :guard (xdoc::tree-listp correspondences))) (let ((__function__ 'xdoc::evmac-topic-design-notes-make-bullets)) (declare (ignorable __function__)) (cond ((endp correspondences) nil) (t (cons (xdoc::li (car correspondences)) (xdoc::evmac-topic-design-notes-make-bullets (cdr correspondences)))))))
Theorem:
(defthm xdoc::tree-listp-of-evmac-topic-design-notes-make-bullets (implies (and (xdoc::tree-listp correspondences)) (b* ((bullets (xdoc::evmac-topic-design-notes-make-bullets correspondences))) (xdoc::tree-listp bullets))) :rule-classes :rewrite)