")
("BID" nil . "") ;begin implementation dependent
("BPAR" nil . "")
; XDOC question: Is
supported? I generate it just below.
; A: it isn't supported, but I'll add support for it.
("BQ" nil . "~%")
("BV" nil . "~%")
("C" nil . "~st")
("EF" nil . "~%")
("EID" nil . "") ;end implementation dependent
("EM" nil . "~st") ;emphasis
("EPAR" nil . "
")
("EQ" nil . "
~%")
("EV" nil . "
~%")
; XDOC question: Is ")
("WARN" nil . "[image]")
; Jared note: these don't seem quite right.
; ("CLICK-HERE" t . "Click here")
; ("PCLICK-HERE" t . "click here")
("CLICK-HERE" t . "Click 
")
; ("LARGE-FLY" t . "
")
; ("WALK" t . "
")
; ("LARGE-WALK" t . "
")
("FLY" t . "[image]")
("LARGE-FLY" t . "[image]")
("WALK" t . "[image]")
("LARGE-WALK" t . "[image]")
; XDOC question: Does this handling of "URL" seem OK? I think it's
; appropriate, rather than @(url ...), since it's not for symbols; but I'm not
; sure.
; A: I think it's probably okay.
("URL" nil . "~st")
)
"Table for use in printing documentation strings, when printing to
an xdoc file. See :DOC markup")
(defconst *xdoc-vp* ; see print-doc-string-part1
'(("BV" "BF") . ("EV" "EF")))
(defconst *xdoc-undocumented-topic*
;; Keep in sync with import-acl2doc.lisp
"acl2::broken-link")
(defun jared-string-upcase-first (x)
;; Upper-case the first letter of a string, if it's lower-case.
;; Most one-liners in the acl2 documentation have lower-case descriptions.
;; I prefer upper-case for xdoc.
(let ((len (length x)))
(if (and (< 0 len)
(standard-char-p (char x 0))
(not (equal (char-upcase (char x 0))
(char x 0))))
(concatenate 'string
(coerce (list (char-upcase (char x 0))) 'string)
(subseq x 1 nil))
x)))
(defun write-a-doc-section (doc-tuple doc-fmt-alist channel state)
; We return an xdoc database entry based on doc-tuple.
(let ((name (if (stringp (nth 0 doc-tuple))
(intern (nth 0 doc-tuple) "ACL2")
(nth 0 doc-tuple)))
(parent (nth 1 doc-tuple))
; See comment below about (nth 2 doc-tuple).
(doc-string (nth 3 doc-tuple)))
(acl2::er-let*
; XDOC change: We avoid writing the header, which would be something like
; "
*xdoc-doc-markup-table* *xdoc-doc-char-subst-table* doc-fmt-alist
channel name t *xdoc-undocumented-topic* nil state)
(get-output-stream-string$ channel state nil)))
; XDOC change: A block of code including a call (print-name-as-link ...)
; normally prints the "Major Section" information that we see on html pages,
; but I'll assume that the xdoc system will manage that sort of thing itself.
(long
(mv-let
(ln state)
(acl2::print-doc-string-part-mv
1 doc-string "" *xdoc-doc-markup-table* *xdoc-doc-char-subst-table*
doc-fmt-alist channel (car doc-tuple) :par
*xdoc-undocumented-topic* *xdoc-vp* state)
; XDOC change: We omit a call (write-doc-menu ...), assuming that the xdoc
; system will take care of menus. But note that our menus include citations
; which will thus probably be missing from the xdoc documentation unless we
; take extra measures. The list of children together with topics collected
; from :cite and :cited-by fields is found in (nth 2 doc-tuple).
(pprogn
(acl2::print-doc-string-part
2 doc-string "" *xdoc-doc-markup-table* *xdoc-doc-char-subst-table*
doc-fmt-alist channel (car doc-tuple) ln *xdoc-undocumented-topic*
*xdoc-vp* state)
(get-output-stream-string$ channel state nil)))))
; XDOC change: unlike the HTML pages, we avoid laying down images that link to
; the documentation's main page and index.
; (write-trailer xdoc-file index-file channel state)
(acl2::value
(list (cons :name name)
(cons :parents (list parent))
(cons :base-pkg
(if (equal (symbol-package-name name) "ACL2-PC")
name
'acl2::rewrite))
(cons :short (jared-string-upcase-first short))
(cons :long long))))))
(defun xdoc-fmt-alist (doc-alist acc)
(cond
((null doc-alist)
acc)
(t (xdoc-fmt-alist
(cdr doc-alist)
(cons (let* ((s (caar doc-alist)))
(list
(cond ((stringp s) s)
(t (let ((name (symbol-name s)))
(cond ((eq s (intern$ name "ACL2"))
name)
(t (concatenate 'string
(symbol-package-name s)
"::"
name))))))
(cons #\p s)
(cons #\c s)))
acc)))))
(defun xdoc-alist1 (doc-alist fmt-alist channel state acc)
(cond ((endp doc-alist) (acl2::value acc))
(t (acl2::er-let*
((entry (write-a-doc-section (car doc-alist) fmt-alist channel
state)))
(xdoc-alist1 (cdr doc-alist) fmt-alist channel state
(cons entry acc))))))
(defun filter-doc-alist (skip-topics doc-alist)
(if (atom doc-alist)
nil
(let* ((doc-tuple (car doc-alist))
(name (if (stringp (nth 0 doc-tuple))
(intern (nth 0 doc-tuple) "ACL2")
(nth 0 doc-tuple))))
(if (member name skip-topics)
(filter-doc-alist skip-topics (cdr doc-alist))
(cons doc-tuple
(filter-doc-alist skip-topics (cdr doc-alist)))))))
(defun write-xdoc-alist-fn (write-p return-p skip-topics state)
(acl2::state-global-let*
((acl2::fmt-hard-right-margin 500 acl2::set-fmt-hard-right-margin)
(acl2::fmt-soft-right-margin 480 acl2::set-fmt-soft-right-margin))
(let ((doc-alist (global-val 'acl2::documentation-alist
(acl2::w state))))
(mv-let
(channel state)
(open-output-channel :string :object state)
(acl2::er-let*
((result (xdoc-alist1 (filter-doc-alist skip-topics doc-alist)
(xdoc-fmt-alist doc-alist nil)
channel state nil)))
(pprogn (close-output-channel channel state)
(cond (write-p (acl2::f-put-global 'acl2::xdoc-alist
result
state))
(t state))
(acl2::value (and return-p result))))))))
(defmacro acl2::write-xdoc-alist (&key (write-p 't)
(return-p 'nil)
(skip-topics 'nil))
`(write-xdoc-alist-fn ,write-p ,return-p ,skip-topics state))
; Utility for accessing element of xdoc-alist:
(defun xdoc-entry-fn (name xdoc-alist)
(cond ((endp xdoc-alist) nil)
((equal name (cdr (assoc-eq :name (car xdoc-alist))))
(car xdoc-alist))
(t (xdoc-entry-fn name (cdr xdoc-alist)))))
(defmacro acl2::xdoc-entry (name)
`(xdoc-entry-fn ',name
(acl2::f-get-global 'acl2::xdoc-alist
state)))