other
(in-package "XDOC")
other
(include-book "fmt-to-str")
other
(include-book "names")
other
(include-book "std/strings/printtree-concat" :dir :system)
other
(local (include-book "std/testing/assert-bang" :dir :system))
other
(set-state-ok t)
other
(program)
error-contextfunction
(defun error-context (x n xl) (declare (type string x)) (b* ((min (nfix (- n 40))) (max (min (+ n 20) xl))) (subseq x min max)))
skip-past-wsfunction
(defun skip-past-ws (x n xl) (declare (type string x)) (cond ((eql xl n) n) ((member (char x n) '(#\ #\ #\ #\ )) (skip-past-ws x (+ 1 n) xl)) (t n)))
parse-symbol-name-partfunction
(defun parse-symbol-name-part (x n xl bar-escape-p slash-escape-p some-chars-p nice-error-msg-p acc) (declare (type string x)) (b* (((when (= xl n)) (b* ((result (rchars-to-string acc)) ((when (or bar-escape-p slash-escape-p (not some-chars-p))) (mv (if nice-error-msg-p (cat "Near " (error-context x n xl) ": unexpected end of string while reading symbol. " "Characters read so far: " result) "Symbol Parse Error") result n))) (mv nil result n))) (n+1 (+ n 1)) (char (char x n)) ((when slash-escape-p) (parse-symbol-name-part x n+1 xl bar-escape-p nil t nice-error-msg-p (cons char acc))) ((when (eql char #\|)) (parse-symbol-name-part x n+1 xl (not bar-escape-p) nil t nice-error-msg-p acc)) ((when (eql char #\\)) (parse-symbol-name-part x n+1 xl bar-escape-p t t nice-error-msg-p acc)) ((when bar-escape-p) (parse-symbol-name-part x n+1 xl t nil t nice-error-msg-p (cons char acc))) ((when (member char '(#\ #\( #\) #\ #\ #\ #\: #\, #\' #\`))) (if some-chars-p (mv nil (rchars-to-string acc) n) (mv (if nice-error-msg-p (cat "Near " (error-context x n xl) ": expected to read some part of a symbol, but found " (implode (list char)) ".") "Symbol Parse Error") "" n))) ((when (or (and (char<= #\a char) (char<= char #\z)))) (parse-symbol-name-part x n+1 xl nil nil t nice-error-msg-p (cons (char-upcase char) acc)))) (parse-symbol-name-part x n+1 xl nil nil t nice-error-msg-p (cons char acc))))
parse-symbolfunction
(defun parse-symbol (x n xl base-pkg kpa nice-error-msg-p) (declare (type string x)) (b* (((when (= xl n)) (mv (if nice-error-msg-p (cat "Near " (error-context x n xl) ": end of string while trying to parse a symbol.") "Symbol Parse Error") nil n)) (char (char x n)) ((when (eql char #\:)) (b* (((mv error name n) (parse-symbol-name-part x (+ n 1) xl nil nil nil nice-error-msg-p nil))) (if error (mv error nil n) (mv nil (intern-in-package-of-symbol name :keyword) n)))) ((mv error part1 n) (parse-symbol-name-part x n xl nil nil nil nice-error-msg-p nil)) ((when error) (mv error nil n)) ((when (and (< (+ n 1) xl) (eql (char x n) #\:) (eql (char x (+ n 1)) #\:))) (b* (((unless (assoc-equal part1 kpa)) (mv (if nice-error-msg-p (cat "Near " (error-context x n xl) ": not a known package: " part1 ".") "Symbol Parse Error") nil n)) ((mv error part2 n) (parse-symbol-name-part x (+ n 2) xl nil nil nil nice-error-msg-p nil)) ((when error) (mv error nil n)) ((when (and (< n xl) (eql (char x n) #\:))) (mv (if nice-error-msg-p (cat "Near " (error-context x n xl) ": Three layers of colons in symbol name?") "Symbol Parse Error") nil n))) (mv nil (intern$ part2 part1) n))) ((when (and (< n xl) (eql (char x n) #\:))) (mv (if nice-error-msg-p (cat "Near " (error-context x n xl) ": Lone colon after symbol name?") "Symbol Parse Error") nil n))) (mv nil (intern-in-package-of-symbol part1 base-pkg) n)))
other
(encapsulate nil (logic) (local (defun test (x expect-errmsg expect-result expect-n-prime) (declare (xargs :mode :program)) (b* ((known-pkgs (pairlis$ '("KEYWORD" "ACL2" "XDOC") nil)) ((mv errmsg result n-prime) (parse-symbol x 0 (length x) 'foo known-pkgs t))) (cw "Errmsg: Found ~x0, expected ~x1~%" errmsg expect-errmsg) (cw "Result: Found ~x0, expected ~x1~%" result expect-result) (cw "N-prime: Found ~x0, expected ~x1~%" n-prime expect-n-prime) (and (or (iff errmsg expect-errmsg) (cw "Errmsg failed!~%")) (or expect-errmsg (equal result expect-result) (cw "Result failed!~%")) (or expect-errmsg (equal n-prime expect-n-prime) (cw "N-Prime failed!~%")))))) (local (progn (assert! (test "foo" nil 'foo 3)) (assert! (test "bar" nil 'bar 3)) (assert! (test "acl2::bar)" nil 'bar 9)) (assert! (test "xdoc::bar)" nil 'bar 9)) (assert! (test "xdoc::|foo|)" nil '|foo| 11)) (assert! (test "xdoc::bar12 " nil 'bar12 11)) (assert! (test ":foo)" nil :foo 4)) (assert! (test ":|foo|)" nil :|foo| 6)) (assert! (test ":||" nil : 3)) (assert! (test "acl2::bar|:|)" nil 'bar\: 12)) (assert! (test ":" t nil nil)) (assert! (test "||:" t nil nil)) (assert! (test "::|foo|)" t nil nil)) (assert! (test "acl2:::bar)" t nil nil)) (assert! (test "acl2::bar:" t nil nil)) (assert! (test "123" nil '123 3)))))
autolink-and-encodefunction
(defun autolink-and-encode (x n xl baseidx topics base-pkg kpa acc) (b* (((when (int= n xl)) (pcat acc (subseq x baseidx n))) (char1 (char x n)) ((when (eql char1 #\<)) (autolink-and-encode x (+ 1 n) xl (+ 1 n) topics base-pkg kpa (pcat acc (subseq x baseidx n) "<"))) ((when (eql char1 #\>)) (autolink-and-encode x (+ 1 n) xl (+ 1 n) topics base-pkg kpa (pcat acc (subseq x baseidx n) ">"))) ((when (eql char1 #\&)) (autolink-and-encode x (+ 1 n) xl (+ 1 n) topics base-pkg kpa (pcat acc (subseq x baseidx n) "&"))) ((when (eql char1 #\")) (autolink-and-encode x (+ 1 n) xl (+ 1 n) topics base-pkg kpa (pcat acc (subseq x baseidx n) """))) ((unless (eql char1 #\()) (autolink-and-encode x (+ 1 n) xl baseidx topics base-pkg kpa acc)) ((mv err symbol n-prime) (parse-symbol x (+ 1 n) xl base-pkg kpa nil)) ((when err) (autolink-and-encode x (+ 1 n) xl baseidx topics base-pkg kpa acc)) (look (hons-get symbol topics)) ((unless look) (autolink-and-encode x (+ 1 n) xl baseidx topics base-pkg kpa acc)) (acc (pcat acc (subseq x baseidx (+ 1 n)) "<see topic="")) (acc (file-name-mangle symbol acc)) (acc (pcat acc "">")) (acc (simple-html-encode-str x (+ 1 n) n-prime acc)) (acc (pcat acc "</see>"))) (autolink-and-encode x n-prime xl n-prime topics base-pkg kpa acc)))
other
(encapsulate nil (logic) (local (defun test (str expect) (declare (xargs :mode :program)) (b* ((topics '(f g h foo bar baz + - top1 top2)) (alist (make-fast-alist (pairlis$ topics nil))) (known-pkgs (pairlis$ '("ACL2" "KEYWORD" "XDOC") nil)) (acc (autolink-and-encode str 0 (length str) 0 alist 'foo known-pkgs nil)) (- (fast-alist-free alist)) (result (printtree->str acc))) (or (equal result expect) (cw "Result: ~x0~%" result) (cw "Expected: ~x0~%" expect))))) (local (progn (assert! (test "foo" "foo")) (assert! (test "foo & bar" "foo & bar")) (assert! (test "foo & bar <baz>" "foo & bar <baz>")) (assert! (test "(foo (+ 1 2))" "(foo (<see topic="COMMON-LISP_____B2">+</see> 1 2))")) (assert! (test "(xdoc::foo (f 1 2))" "(<see topic="XDOC____FOO">xdoc::foo</see> (<see topic="ACL2____F">f</see> 1 2))")))))
xml-ppr-obj-auxfunction
(defun xml-ppr-obj-aux (x topics-fal base-pkg state acc) (b* ((kpa (known-package-alist state)) (str (fmt-to-str x base-pkg)) (acc (autolink-and-encode str 0 (length str) 0 topics-fal base-pkg kpa acc))) acc))
xml-ppr-obj-fnfunction
(defun xml-ppr-obj-fn (x topics-fal base-pkg state) (printtree->str (xml-ppr-obj-aux x topics-fal base-pkg state nil)))
xml-ppr-objmacro
(defmacro xml-ppr-obj (x &key (state 'state) (topics-fal 'nil) (base-pkg ''foo)) `(b* ((acc (xml-ppr-obj-aux ,XDOC::X ,XDOC::TOPICS-FAL ,XDOC::BASE-PKG ,XDOC::STATE nil)) (ret (printtree->str acc))) ret))
other
(local (progn (assert! (equal (xml-ppr-obj '(f 1 2) :topics-fal (make-fast-alist '((f)))) "(<see topic="XDOC____F">xdoc::f</see> 1 2)")) (assert! (equal (xml-ppr-obj '(f 1 2) :topics-fal (make-fast-alist '((f))) :base-pkg 'foo) "(<see topic="XDOC____F">f</see> 1 2)"))))