   ;;                  #'fstar--eldoc-function)
   (kill-local-variable 'eldoc-documentation-function))
 
-;;; xref-like features
+;;;; xref-like features
 
 (defun fstar--save-point ()
   "Save current position in mark ring and xref stack."


(defun fstar--jump-to-definition-continuation (info)
  "Jump to position in INFO."
  (pcase-let* ((target-fname (fstar-pos-info-source-file info))
               (`(,target-row . ,target-col) (fstar-pos-info-def-start info)))
    (fstar--save-point)
    (catch 'not-found
      (unless (equal target-fname "<input>")
        (unless (file-exists-p target-fname)
          (message "File not found: %S" target-fname)
          (throw 'not-found nil))
        (find-file target-fname))
      (fstar--goto target-row target-col)
      (recenter)
      (pulse-momentary-highlight-one-line (point)))))

(defun fstar-jump-to-definition ()
  "Jump to definition of identifier at point, if any."
  (interactive)
  (cond
   ((not fstar-compat--can-use-info)
    (user-error "This feature isn't available in F* < 0.9.4.1"))
   (fstar-subp--continuation
    (user-error "F* seems busy; please wait until processing is complete"))
   ((not (fstar-subp-live-p))
    (user-error "Please start F* before jumping to a definition"))
   (t (fstar-subp--query (fstar-subp--info-query (point))
                         (apply-partially #'fstar-subp--info-continuation
                                          #'fstar--jump-to-definition-continuation
                                          (point))))))

;;;; Starting the F* subprocess



(defun fstar-subp--info-continuation (continuation pos success response)
  "Handle the results (SUCCESS and RESPONSE) of an #info query at POS.
If response is valid, forward results to CONTINUATION.  With nil
POS, this function can also handle results of #info-fqn queries."
  (if (and success
           (or (null pos) (eq (point) pos)) ;; Point didn't move since request
           (string-match fstar-subp--info-response-regex response))
      (funcall continuation
               (make-fstar-pos-info
                :source-file (match-string 1 response)
                :def-start (cons (string-to-number (match-string 2 response))
                                 (string-to-number (match-string 3 response)))
                :def-end (cons (string-to-number (match-string 4 response))
                               (string-to-number (match-string 5 response)))
                :type (string-trim (substring response (match-end 0)))))
    (funcall continuation nil)))

(defun fstar--eldoc-continuation (info)
  "Display INFO as an eldoc message."
  (when info
    (eldoc-message (fstar-highlight-string (fstar-pos-info-type info)))))

(defun fstar--eldoc-function ()
  "Issue a #info query for current point.
