display

(defun sgr-prefix
  (n)
  (concatenate 'string *sgr-prefix* n "m"))

(defun xdoc-tag-alist-fancy-p
  (val)
  (or (null val)
    (equal val "")
    (string-equal val "FANCY")))

(defun xdoc-tag-alist
  (state)
  (declare (xargs :guard t))
  (b* (((er val) (getenv$ "ACL2_XDOC_TAGS" state)))
    (value (cond ((xdoc-tag-alist-fancy-p val) *xdoc-tag-alist-fancy*)
        ((string-equal val "SIMPLE") *xdoc-tag-alist-simple*)
        ((string-equal val "PLAIN") *xdoc-tag-alist-plain*)
        (t (er hard
            'update-tags-display
            "When environment variable ACL2_XDOC_TAGS has a non-empty ~
                    value, that value must be (up to case) ~v0.  The value ~
                    ~x1 is thus illegal.  See :DOC terminal."
            '("FANCY" "SIMPLE" "PLAIN")
            val))))))

(defun topic-to-rendered
  (topic topic-to-rendered-table)
  (cdr (hons-get (intern topic "ACL2")
      topic-to-rendered-table)))

(defun print-missing-topic-name
  (name)
  (wormhole-eval 'xdoc-missing-link
    '(lambda (whs)
      (set-wormhole-data whs
        (cons name (wormhole-data whs))))
    nil))

(defun left-bracket-start
  (text bound)
  (let ((p (search "[" text :from-end t :end2 bound)))
    (and p
      (cond ((eql p 0) 0)
        ((eql (char text (1- p)) *escape-char*) (left-bracket-start text (1- p)))
        (t p)))))

(defun text-matches-mangle
  (text mangle topic-to-rendered-table)
  (let* ((bracket-posn (left-bracket-start text (length text))) (start (and bracket-posn (1+ bracket-posn)))
      (rendered (and start
          (topic-to-rendered mangle
            topic-to-rendered-table))))
    (cond ((null start) nil)
      ((null rendered) (print-missing-topic-name (subseq text start (length text))))
      (t (let* ((text-topic0 (subseq text start (length text))) (acl2-prefix-posn (search "acl2::" text-topic0 :test 'char-equal))
            (text-topic (if acl2-prefix-posn
                (subseq text-topic0 6 (length text-topic0))
                text-topic0)))
          (cond ((string-equal rendered text-topic) (if acl2-prefix-posn
                (list text-topic)
                t))
            (t (let ((posn (search "::" rendered)))
                (cond ((and posn
                     (string-equal (subseq rendered
                         (+ posn 2)
                         (length rendered))
                       text-topic0)) (list (concatenate 'string
                        (string-downcase (subseq rendered 0 (+ posn 2)))
                        text-topic0)))
                  (t rendered))))))))))

(defun fix-close-see
  (str bracket-posn match)
  (cond ((null bracket-posn) str)
    ((null match) (concatenate 'string
        (subseq str 0 bracket-posn)
        (subseq str
          (1+ bracket-posn)
          (length str))))
    ((stringp match) (concatenate 'string
        (subseq str 0 bracket-posn)
        (subseq str
          (1+ bracket-posn)
          (length str))
        " (see ["
        match
        "])"))
    (t (assert$ (consp match)
        (concatenate 'string
          (subseq str 0 (1+ bracket-posn))
          (car match)
          "]")))))

(defun skip-to-close
  (tag x)
  (cond ((atom x) x)
    (t (b* ((tok1 (car x)) (name (and (closetok-p tok1)
              (closetok-name tok1))))
        (cond ((equal name tag) (cdr x))
          (t (skip-to-close tag (cdr x))))))))

(defun translate-entities-to-plaintext-aux
  (x n xl acc)
  "Returns (MV ERR ACC)"
  (b* (((when (>= n xl)) (mv nil acc)) (char1 (char x n))
      ((when (eql char1 #\&)) (b* (((mv err n tok) (read-entity x n xl)) ((when err) (mv err nil))
            (plaintext (entitytok-as-plaintext tok))
            (acc (revappend-chars plaintext acc)))
          (translate-entities-to-plaintext-aux x
            n
            xl
            acc)))
      (acc (cons char1 acc)))
    (translate-entities-to-plaintext-aux x
      (+ 1 n)
      xl
      acc)))

(defun translate-entities-to-plaintext
  (x)
  "Returns (MV ERR PLAINTEXT-STR)"
  (b* (((mv err acc) (translate-entities-to-plaintext-aux x
         0
         (length x)
         nil)))
    (mv err (rchars-to-string acc))))

(defun translate-att-to-plaintext
  (ctx x)
  (b* (((mv err text) (translate-entities-to-plaintext x)) ((when err) (er hard?
          'translate-att-to-plaintext
          "Error in ~s0: ~s1~%"
          ctx
          err)
        ""))
    text))

(defun push-tstk
  (tok tstk)
  (cond ((null tstk) tok)
    (t (cons tok tstk))))

(defun pop-tstk
  (tstk)
  (cond ((atom tstk) nil)
    ((eq (car tstk) :text) nil)
    (t (cdr tstk))))

(defun accumulate-tstk
  (tstk rest)
  (cond ((atom tstk) rest)
    ((eq (car tstk) :text) (cons tstk rest))
    (t (accumulate-tstk (cdr tstk)
        (cons (car tstk) rest)))))

(defun merge-text
  (x acc
    codes
    href
    topic-to-rendered-table
    xdoc-tag-alist
    imgp
    tstk)
  (b* (((when (atom x)) acc) (tok1 (car x))
      (rest (cdr x))
      ((when (opentok-p tok1)) (b* ((name (opentok-name tok1)) (codes (if (equal name "code")
                (+ 1 codes)
                codes)))
          (cond ((equal name "img") (b* ((tok (list :text (cond (imgp (concatenate 'string
                           *img-prefix*
                           (cdr (assoc-equal "src" (opentok-atts tok1)))
                           *img-suffix*))
                       (t "{IMAGE}")))))
                (merge-text (cons tok rest)
                  acc
                  codes
                  href
                  topic-to-rendered-table
                  xdoc-tag-alist
                  imgp
                  tstk)))
            ((equal name "icon") (b* ((tok (list :text "{ICON}")))
                (merge-text (cons tok rest)
                  acc
                  codes
                  href
                  topic-to-rendered-table
                  xdoc-tag-alist
                  imgp
                  tstk)))
            ((equal name "a") (b* ((href (cdr (assoc-equal "href" (opentok-atts tok1)))) (tok (list :text (cat "{"))))
                (merge-text (cons tok rest)
                  acc
                  codes
                  href
                  topic-to-rendered-table
                  xdoc-tag-alist
                  imgp
                  tstk)))
            ((equal name "see") (b* ((href (or href
                     (cdr (assoc-equal "topic" (opentok-atts tok1))))) (tok (list :text "[")))
                (merge-text (cons tok rest)
                  acc
                  codes
                  href
                  topic-to-rendered-table
                  xdoc-tag-alist
                  imgp
                  tstk)))
            ((equal name "srclink") (b* ((tok (list :text "<")))
                (merge-text (cons tok rest)
                  acc
                  codes
                  href
                  topic-to-rendered-table
                  xdoc-tag-alist
                  imgp
                  tstk)))
            (t (let ((entry (assoc-equal name xdoc-tag-alist)))
                (cond ((null entry) (merge-text rest
                      (cons tok1 acc)
                      codes
                      href
                      topic-to-rendered-table
                      xdoc-tag-alist
                      imgp
                      tstk))
                  ((null (cdr entry)) (merge-text rest
                      acc
                      codes
                      nil
                      topic-to-rendered-table
                      xdoc-tag-alist
                      imgp
                      tstk))
                  ((null (cddr entry)) (b* ((tok (list :text (cadr entry))))
                      (merge-text (cons tok (skip-to-close name x))
                        acc
                        codes
                        href
                        topic-to-rendered-table
                        xdoc-tag-alist
                        imgp
                        tstk)))
                  (t (b* ((tok (list :text (cadr entry))))
                      (merge-text (cons tok rest)
                        acc
                        codes
                        href
                        topic-to-rendered-table
                        xdoc-tag-alist
                        imgp
                        (push-tstk tok tstk))))))))))
      ((when (closetok-p tok1)) (b* ((name (closetok-name tok1)) (codes (if (equal name "code")
                (- 1 codes)
                codes))
            (entry (assoc-equal name xdoc-tag-alist)))
          (cond (entry (cond ((null (cdr entry)) (merge-text rest
                    acc
                    codes
                    href
                    topic-to-rendered-table
                    xdoc-tag-alist
                    imgp
                    tstk))
                ((null (cddr entry)) (merge-text rest
                    acc
                    codes
                    href
                    topic-to-rendered-table
                    xdoc-tag-alist
                    imgp
                    tstk))
                (t (b* ((tok (list :text (cddr entry))) (tstk (pop-tstk tstk)))
                    (merge-text (cons tok (accumulate-tstk tstk rest))
                      acc
                      codes
                      href
                      topic-to-rendered-table
                      xdoc-tag-alist
                      imgp
                      tstk)))))
            ((member-equal name '("see")) (b* ((text (texttok-text (car acc))) (bracket-posn (left-bracket-start text (length text)))
                  (match (assert$ bracket-posn
                      (and href
                        (consp acc)
                        (texttok-p (car acc))
                        (text-matches-mangle text
                          href
                          topic-to-rendered-table)))))
                (cond ((eq match t) (let ((tok (list :text "]")))
                      (merge-text (cons tok rest)
                        acc
                        codes
                        nil
                        topic-to-rendered-table
                        xdoc-tag-alist
                        imgp
                        tstk)))
                  (t (merge-text rest
                      (cons (list :text (fix-close-see text
                            bracket-posn
                            match))
                        (cdr acc))
                      codes
                      nil
                      topic-to-rendered-table
                      xdoc-tag-alist
                      imgp
                      tstk)))))
            ((member-equal name '("a")) (let* ((href-plain (if href
                     (translate-att-to-plaintext 'href href)
                     "")) (tok (list :text (cat " | " href-plain "}"))))
                (merge-text (cons tok rest)
                  acc
                  codes
                  nil
                  topic-to-rendered-table
                  xdoc-tag-alist
                  imgp
                  tstk)))
            ((equal name "srclink") (let ((tok (list :text ">")))
                (merge-text (cons tok rest)
                  acc
                  codes
                  href
                  topic-to-rendered-table
                  xdoc-tag-alist
                  imgp
                  tstk)))
            (t (merge-text rest
                (cons tok1 acc)
                codes
                href
                topic-to-rendered-table
                xdoc-tag-alist
                imgp
                tstk)))))
      (tok1 (cond ((entitytok-p tok1) (list :text (entitytok-as-plaintext tok1)))
          ((zp codes) (list :text (normalize-whitespace (texttok-text tok1))))
          (t tok1)))
      ((unless (texttok-p (car acc))) (merge-text rest
          (cons tok1 acc)
          codes
          href
          topic-to-rendered-table
          xdoc-tag-alist
          imgp
          tstk))
      (merged-tok (list :text (cons (texttok-texttree (car acc))
            (texttok-texttree tok1)))))
    (merge-text rest
      (cons merged-tok (cdr acc))
      codes
      href
      topic-to-rendered-table
      xdoc-tag-alist
      imgp
      tstk)))

(defun has-tag-above
  (tag open-tags)
  (if (atom open-tags)
    nil
    (or (equal tag (opentok-name (car open-tags)))
      (has-tag-above tag (cdr open-tags)))))

(defun get-indent-level
  (open-tags)
  (b* (((when (atom open-tags)) 0) (name (opentok-name (car open-tags)))
      ((when (member-equal name '("h1" "h2" "h3"))) 0)
      ((when (member-equal name
           '("p" "short" "h4" "h5" "index_entry"))) (+ 2 (get-indent-level (cdr open-tags))))
      ((when (member-equal name '("index_body"))) (+ 4 (get-indent-level (cdr open-tags))))
      ((when (member-equal name '("ol" "ul"))) (if (has-tag-above "li" open-tags)
          (+ 4 (get-indent-level (cdr open-tags)))
          (+ 6 (get-indent-level (cdr open-tags)))))
      ((when (equal name "dt")) (+ 4 (get-indent-level (cdr open-tags))))
      ((when (equal name "dd")) (+ 6 (get-indent-level (cdr open-tags))))
      ((when (equal name "code")) (+ 4 (get-indent-level (cdr open-tags))))
      ((when (equal name "math")) (+ 4 (get-indent-level (cdr open-tags))))
      ((when (equal name "blockquote")) (+ 4 (get-indent-level (cdr open-tags))))
      ((when (member-equal name '("table"))) (+ 4 (get-indent-level (cdr open-tags)))))
    (get-indent-level (cdr open-tags))))

(defun get-list-type
  (open-tags)
  (b* (((when (atom open-tags)) :bulleted) (name (opentok-name (car open-tags)))
      ((when (equal name "ol")) :numbered)
      ((when (equal name "ul")) :bulleted))
    (get-list-type (cdr open-tags))))

(defun auto-indent
  (acc open-tags)
  (append (make-list (get-indent-level open-tags)
      :initial-element #\ )
    acc))

(defun maybe-newline
  (acc)
  (b* ((acc (remove-spaces-from-front acc)) (acc (if (or (atom acc) (eql (car acc) #\
))
          acc
          (cons #\
 acc))))
    acc))

(defun maybe-doublespace
  (acc)
  (b* ((acc (remove-spaces-from-front acc)) ((when (atom acc)) acc)
      ((unless (eql (car acc) #\
)) (list* #\
 #\
 acc))
      (acc (remove-spaces-from-front (cdr acc)))
      ((when (atom acc)) acc)
      ((unless (eql (car acc) #\
)) (list* #\
 #\
 acc)))
    (cons #\
 acc)))

(defun maybe-triplespace
  (acc)
  (b* ((acc (remove-spaces-from-front acc)) ((when (atom acc)) acc)
      ((unless (eql (car acc) #\
)) (list* #\
 #\
 #\
 acc))
      (acc (remove-spaces-from-front (cdr acc)))
      ((when (atom acc)) acc)
      ((unless (eql (car acc) #\
)) (list* #\
 #\
 #\
 acc))
      (acc (remove-spaces-from-front (cdr acc)))
      ((when (atom acc)) acc)
      ((unless (eql (car acc) #\
)) (list* #\
 #\
 #\
 acc)))
    (list* #\
 #\
 acc)))

(defun prepend-each-line
  (spaces x n xl acc)
  (b* (((when (>= n xl)) acc) (char-n (char x n))
      ((unless (eql char-n #\
)) (prepend-each-line spaces
          x
          (+ 1 n)
          xl
          (cons char-n acc)))
      (acc (remove-spaces-from-front acc))
      (acc (cons #\
 acc))
      (acc (append spaces acc)))
    (prepend-each-line spaces
      x
      (+ 1 n)
      xl
      acc)))

(defun tokens-to-terminal
  (tokens wrap-col
    open-tags
    list-nums
    acc)
  (b* (((when (atom tokens)) acc) (tok1 (car tokens))
      (rest (cdr tokens))
      ((when (opentok-p tok1)) (b* ((name (opentok-name tok1)) (open-tags (cons tok1 open-tags))
            (list-nums (cond ((member-equal name '("ol" "ul")) (cons 0 list-nums))
                ((equal name "li") (cons (+ 1 (nfix (car list-nums)))
                    (cdr list-nums)))
                (t list-nums)))
            (acc (cond ((equal name "li") (b* ((bullet (if (eq (get-list-type open-tags) :bulleted)
                         "* "
                         (cat (nat-to-dec-string (nfix (car list-nums)))
                           ". "))) (bullet-len (length bullet))
                      (desired (get-indent-level open-tags))
                      (spaces (make-list (nfix (- desired bullet-len))
                          :initial-element #\ ))
                      (acc (maybe-doublespace acc))
                      (acc (append spaces acc))
                      (acc (revappend-chars bullet acc)))
                    acc))
                ((member-equal name
                   '("h4" "h5"
                     "p"
                     "li"
                     "dt"
                     "dd"
                     "br"
                     "index_head"
                     "index_body"
                     "blockquote")) (auto-indent (maybe-newline acc)
                    open-tags))
                ((member-equal name
                   '("code" "math" "short" "long")) (auto-indent (maybe-doublespace acc)
                    open-tags))
                ((member-equal name '("h1" "h2" "h3")) (auto-indent (maybe-triplespace acc)
                    open-tags))
                ((member-equal name '("table")) (auto-indent (maybe-newline acc)
                    open-tags))
                ((equal name "index") (b* ((atts (opentok-atts tok1)) (title (cdr (assoc-equal "title" atts)))
                      (title (if (stringp title)
                          title
                          "??? title ???"))
                      (acc (maybe-triplespace acc))
                      (acc (revappend-chars title acc))
                      (acc (maybe-doublespace acc)))
                    acc))
                (t acc))))
          (tokens-to-terminal rest
            wrap-col
            open-tags
            list-nums
            acc)))
      ((when (closetok-p tok1)) (b* ((name (closetok-name tok1)) (open-tags (cdr open-tags))
            (list-nums (if (member-equal name '("ol" "ul"))
                (cdr list-nums)
                list-nums))
            (acc (cond ((member-equal name
                   '("h1" "h2"
                     "h3"
                     "h4"
                     "h5"
                     "p"
                     "dl"
                     "ul"
                     "ol"
                     "short"
                     "code"
                     "math"
                     "index"
                     "index_body"
                     "blockquote"
                     "table")) (auto-indent (maybe-doublespace acc)
                    open-tags))
                ((member-equal name
                   '("li" "dd" "dt" "index_head" "tr")) (auto-indent (maybe-newline acc)
                    open-tags))
                ((member-equal name '("td" "th")) (list* #\  #\  #\| #\	 acc))
                (t acc))))
          (tokens-to-terminal rest
            wrap-col
            open-tags
            list-nums
            acc)))
      (text (texttok-text tok1))
      (codep (has-tag-above "code" open-tags))
      (level (get-indent-level open-tags))
      (acc (if codep
          (b* ((len (length text)) (starts-with-newline-p (and (> len 0) (eql (char text 0) #\
)))
              (start-from (if starts-with-newline-p
                  1
                  0)))
            (prepend-each-line (make-list level :initial-element #\ )
              text
              start-from
              (length text)
              acc))
          (let ((wrapped (word-wrap-paragraph text
                 level
                 wrap-col)))
            (revappend-chars wrapped acc)))))
    (tokens-to-terminal rest
      wrap-col
      open-tags
      list-nums
      acc)))

(defun revappend-full-symbol
  (sym ans)
  (b* ((ans (revappend-chars (symbol-package-name sym)
         ans)) (ans (revappend-chars "::" ans))
      (ans (revappend-chars (symbol-name sym) ans)))
    ans))

(defun revappend-parents
  (parents ans)
  (b* (((when (atom parents)) ans) ((when (atom (cdr parents))) (revappend-full-symbol (car parents) ans))
      (ans (revappend-full-symbol (car parents) ans))
      (ans (if (consp (cddr parents))
          (revappend-chars ", " ans)
          (revappend-chars " and " ans))))
    (revappend-parents (cdr parents) ans)))

(defun render-sym
  (sym)
  (let ((str (symbol-name sym)))
    (if (eq (intern str "ACL2") sym)
      (rendered-name str)
      (concatenate 'string
        (symbol-package-name sym)
        "::"
        (rendered-name str)))))

(defun acl2-broken-links-alist-to-rendered-table-init
  (alist acc)
  (cond ((endp alist) acc)
    (t (acl2-broken-links-alist-to-rendered-table-init (cdr alist)
        (acons (intern (url (caar alist)) "ACL2")
          (render-sym (caar alist))
          acc)))))

(defun topic-to-rendered-table-init-1
  (table acc)
  (cond ((endp table) acc)
    (t (topic-to-rendered-table-init-1 (cdr table)
        (let ((name (cdr (assoc-eq :name (car table)))))
          (acons (intern (url name) "ACL2")
            (render-sym name)
            acc))))))

(defun topic-to-rendered-table-init
  (state)
  (let ((pair (and (f-boundp-global 'topic-to-rendered-pair state)
         (f-get-global 'topic-to-rendered-pair state))))
    (er-let* ((table (all-xdoc-topics state)))
      (cond ((equal (car pair) table) (value (cdr pair)))
        (t (prog2$ (and pair (fast-alist-free (cdr pair)))
            (let* ((cval (defined-constant '*acl2-broken-links-alist*
                   (w state))) (alist0 (assert$ (or (null cval) (quotep cval))
                    (acl2-broken-links-alist-to-rendered-table-init (unquote cval)
                      nil)))
                (fal (make-fast-alist (topic-to-rendered-table-init-1 table
                      alist0)))
                (state (f-put-global 'topic-to-rendered-pair
                    (cons table fal)
                    state)))
              (value fal))))))))

(defun render-images
  (state)
  (mv-let (erp val state)
    (getenv$ "ACL2_DOC_IMAGES" state)
    (declare (ignore erp))
    (mv (and val (not (equal val "")))
      state)))

(defun topic-to-text
  (x all-topics state)
  "Returns (MV TEXT STATE)"
  (b* ((name (cdr (assoc :name x))) (topics-fal (topics-fal all-topics))
      ((mv text state) (preprocess-topic (acons :parents nil x)
          all-topics
          topics-fal
          t
          state))
      (- (fast-alist-free topics-fal))
      ((mv err tokens) (parse-xml text))
      ((when err) (mv (cat "Error displaying xdoc topic: "
            *nls*
            *nls*
            err
            *nls*
            *nls*)
          state))
      ((mv err
         topic-to-rendered-table
         state) (topic-to-rendered-table-init state))
      ((when err) (mv (cat "Error displaying xdoc topic: "
            *nls*
            *nls*
            err
            *nls*
            *nls*)
          state))
      ((mv - xdoc-tag-alist state) (xdoc-tag-alist state))
      ((mv imgp state) (render-images state))
      (merged-tokens (reverse (merge-text tokens
            nil
            0
            nil
            topic-to-rendered-table
            xdoc-tag-alist
            imgp
            nil)))
      (terminal (rchars-to-string (tokens-to-terminal merged-tokens
            70
            nil
            nil
            nil)))
      (ans nil)
      (ans (revappend-chars (symbol-package-name name)
          ans))
      (ans (revappend-chars "::" ans))
      (ans (revappend-chars (symbol-name name) ans))
      (from (cdr (assoc :from x)))
      (ans (if from
          (b* ((ans (revappend-chars " -- " ans)) (ans (revappend-chars from ans))
              (ans (cons #\
 ans)))
            ans)
          ans))
      (parents (cdr (assoc :parents x)))
      (ans (if parents
          (b* ((ans (revappend-chars "Parents: " ans)) (ans (revappend-parents parents ans))
              (ans (list* #\
 #\. ans)))
            ans)
          ans))
      (ans (cons #\
 ans))
      (ans (revappend-chars terminal ans))
      (ans (cons #\
 ans)))
    (mv (rchars-to-string ans) state)))

(defun warn-on-missing-topic-names
  (state)
  (cond ((warning-off-p "xdoc-link" state) nil)
    (t (wormhole-eval 'xdoc-missing-link
        '(lambda (whs)
          (let ((data (wormhole-data whs)))
            (and data
              (warning$-cw0 'xdoc
                nil
                (default-state-vars t)
                "Please note the following broken topic link ~
                        name~#0~[~/s~]: ~&0.  To suppress such warnings: ~x1."
                (reverse (remove-duplicates-equal data))
                '(toggle-inhibit-warning "xdoc-link")))))
        nil))))

(defun display-topic
  (x all-topics state)
  (b* (((mv text state) (topic-to-text x all-topics state)) (state (princ$ text *standard-co* state)))
    (prog2$ (warn-on-missing-topic-names state)
      state)))

(defun summarize-nearby-topic
  (x state)
  (b* ((name (cdr (assoc :name x))) (base-pkg (cdr (assoc :base-pkg x)))
      (short (cdr (assoc :short x)))
      ((mv short-acc state) (preprocess-main short
          name
          nil
          nil
          base-pkg
          state
          nil))
      (short (printtree->str short-acc))
      ((mv err tokens) (parse-xml short))
      ((when err) (cw "Error summarizing xdoc topic:~%~%")
        (b* ((state (princ$ err *standard-co* state)) (state (newline *standard-co* state))
            (state (newline *standard-co* state)))
          state))
      ((mv err
         topic-to-rendered-table
         state) (topic-to-rendered-table-init state))
      ((when err) (cw "Error summarizing xdoc topic:~%~%")
        (b* ((state (princ$ err *standard-co* state)) (state (newline *standard-co* state))
            (state (newline *standard-co* state)))
          state))
      ((mv - xdoc-tag-alist state) (xdoc-tag-alist state))
      ((mv imgp state) (render-images state))
      (merged-tokens (reverse (merge-text tokens
            nil
            0
            nil
            topic-to-rendered-table
            xdoc-tag-alist
            imgp
            nil)))
      (terminal (rchars-to-string (tokens-to-terminal merged-tokens
            70
            nil
            nil
            nil)))
      (state (princ$ "    " *standard-co* state))
      (state (princ$ (symbol-package-name name)
          *standard-co*
          state))
      (state (princ$ "::" *standard-co* state))
      (state (princ$ (symbol-name name)
          *standard-co*
          state))
      (state (newline *standard-co* state))
      (state (princ$ (prefix-lines terminal "      ")
          *standard-co*
          state))
      (state (newline *standard-co* state)))
    state))

(defun summarize-nearby-topics
  (x state)
  (if (atom x)
    state
    (pprogn (summarize-nearby-topic (car x) state)
      (summarize-nearby-topics (cdr x) state))))

(defun find-topics
  (names all-topics)
  (if (atom names)
    nil
    (cons (find-topic (car names) all-topics)
      (find-topics (cdr names) all-topics))))

(defun all-topic-names
  (topics)
  (if (atom topics)
    nil
    (cons (cdr (assoc :name (car topics)))
      (all-topic-names (cdr topics)))))

(defun suggest-alternatives
  (name all-topics state)
  (declare (xargs :guard (symbolp name)))
  (b* ((topic-names (all-topic-names all-topics)) (suggestions (xdoc-autocorrect name topic-names))
      (- (cw "~%Argh!  No documentation for ~s0::~s1.~%"
          (symbol-package-name name)
          (symbol-name name)))
      ((unless suggestions) state)
      (- (if (eql (len suggestions) 1)
          (cw "Hrmn, maybe you wanted this one:~%~%")
          (cw "Hrmn, maybe you wanted one of these:~%~%")))
      (suggested-topics (find-topics suggestions all-topics))
      (state (summarize-nearby-topics suggested-topics
          state))
      (state (newline *standard-co* state)))
    state))

(defun colon-xdoc-fn
  (name all-topics state)
  (declare (xargs :guard (symbolp name)))
  (b* ((xdoc-entry (find-topic name all-topics)) ((when (not xdoc-entry)) (let ((state (suggest-alternatives name
               all-topics
               state)))
          (value :invisible)))
      (state (display-topic xdoc-entry
          all-topics
          state)))
    (value :invisible)))