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)))