          (type (fstar-lookup-result-type info))
          (def (fstar-lookup-result-def info))
          (name (fstar-lookup-result-name info))
-         (def-loc (fstar-lookup-result-def-loc-str info))
-         (title (fstar--propertize-title name))
-         (subtitle (propertize def-loc 'face '(:height 0.9))))
+         (def-loc (fstar-lookup-result-def-loc info))
+         (def-loc-str (fstar-lookup-result-def-loc-str info))
+         (title (fstar--propertize-title name)))
     (save-excursion
-      (insert title "\n" subtitle)
+      (insert title "\n")
+      (fstar--insert-link def-loc-str def-loc '(:height 0.9 :inherit link))
       (fstar--doc-buffer-populate-1 "Type"
         (and type (fstar-highlight-string type)))
       (fstar--doc-buffer-populate-1 "Definition"

    (insert (fstar--propertize-title title) "\n\n"))
  (dolist (fname deps)
    (insert "  ")
    (insert-text-button fname 'fstar--target fname
                        'face 'default 'follow-link t
                        'action 'fstar--visit-link-target)
    (insert "\n")))

(defun fstar-subp--visit-dependency-continuation (source-buf status response)


(defun fstar--visit-link-target (marker)
  "Jump to file indicated by entry at MARKER."
  (let* ((pos (marker-position marker))
         (buf (marker-buffer marker))
         (target (get-text-property pos 'fstar--target buf)))
    (cond
     ((stringp target)
      (find-file target))
     ((fstar-location-p target)
      (fstar--navigate-to (fstar-location-filename target)
                     (fstar-location-line-from target)
                     (fstar-location-col-from target))))))

(defun fstar--insert-link (label target face)
  "Insert a link to TARGET with LABEL and FACE.
TARGET is either a string or a location."
  (insert-text-button label 'fstar--target target
                      'face face 'follow-link t
                      'action 'fstar--visit-link-target))

(defun fstar--lispify-null (x)
  "Return X, or nil if X is `:json-null'."
