           (and help-kbd (fstar-lookup-result-doc info)
                (substitute-command-keys (format " (%s for help)" help-kbd)))))
 
+(defun fstar-lookup-result-def-loc (info)
+  "Format a location information from INFO."
+  (format "%s:%d:%d"
+          (fstar-lookup-result-source-file info) ;; FIXME hyperlink
+          (car (fstar-lookup-result-def-start info))
+          (cdr (fstar-lookup-result-def-start info))))
 
 (defun fstar-lookup-result-docstring (info)
   "Format docstring of INFO, if any."


(defconst fstar--doc-buffer-name "*fstar-doc*")

(defun fstar--doc-at-point-continuation (info)
  "Show documentation in INFO."
  (-if-let* ((doc (and info (fstar-lookup-result-doc info))))
      (with-help-window fstar--doc-buffer-name
        (with-current-buffer standard-output
          (insert (fstar--unwrap-paragraphs (string-trim doc)))
          (fstar--highlight-docstring-buffer)))
    (message
     (substitute-command-keys "No documentation found. \
Try visiting the source file with \\[fstar-jump-to-definition]?"))))

(defun fstar-doc-at-point-dwim ()
  "Show documentation of identifier at point, if any."

(defun fstar-subp-company--doc-buffer-continuation (callback info)
  "Forward documentation INFO to CALLBACK.
CALLBACK is the company-mode asynchronous doc-buffer callback."
  (funcall callback (when info
                      (with-current-buffer
                          (get-buffer-create "*company-documentation*")
                        (erase-buffer)
                        (fstar--doc-buffer-populate info)
                        (current-buffer)))))

(defun fstar-subp-company--async-doc-buffer (candidate callback)
  "Find documentation of CANDIDATE and pass it to CALLBACK."
