         (with-selected-window win
           (with-current-buffer buf ;; FIXME check this
             (push-mark (point) t) ;; Save default position in mark ring
-	    (setq fstar--parent-buffer parent-buf)
+            (setq fstar--parent-buffer parent-buf)
             (fstar--goto-line-col (or line 1) col)
             (recenter)
             (when line

  "Return a live fstar process if available in some buffer.
Raise an error with ERROR-FN if a live F* process isn't available anywhere."
  (cl-loop for buf in `(,(current-buffer) ,fstar--parent-buffer ,@(buffer-list))
	   for proc = (and buf
			   (eq (buffer-local-value 'major-mode buf) 'fstar-mode)
			   (buffer-local-value 'fstar-subp--process buf))
	   when (and proc (fstar-subp-live-p proc))
	   return buf))

(defun fstar-subp--serialize-query (query id)
  "Serialize QUERY with ID to JSON."

DISPLAY-ACTION indicates how: nil means in the current window;
`window' means in a side window."
  (-if-let* ((def-loc (and (fstar-lookup-result-p info)
                           (fstar-lookup-result-def-loc info))))
      (with-current-buffer cur-buf
        (fstar--navigate-to def-loc display-action))
    (message "No definition found")))

(defun fstar-jump-to-definition-1 (pos disp)
