Gen-xdoc-for-file
Generate xdoc using textual definitions from a .lisp file.
;; Generate xdoc topics for the given ITEMS, each of which is a doublet of a
;; name and its :short xdoc string. The body of each generated xdoc topic will
;; contain the block of lines (demarcated by empty lines) from the given
;; FILENAME that defines the given name. Each name must be defined in a defun,
;; defund, defmacro, defthm, defthmd, or define.
(defmacro gen-xdoc-for-file (filename
items
parents)
`(make-event (gen-xdoc-for-file-fn ',filename ',items ',parents state)))
