                 (insert replacement)))))))
     (buffer-substring-no-properties (point-min) (point-max))))
 
-(defun fstar-subp--column-number-at-pos (pos)
-  "Return column number at POS."
-  (save-excursion (goto-char pos) (- (point) (point-at-bol))))
-
 (defun fstar-subp--push-header (pos lax)
   "Prepare a header for a region starting at POS.
 With non-nil LAX, the region is to be processed in lax mode."

             (process-connection-type nil)
             (args (fstar-subp-with-interactive-args (fstar-subp-get-prover-args)))
             (proc (fstar-subp-start-process buf prog-abs args)))
        (fstar-subp-log "Started F* interactive with arguments %S" args)
        (set-process-query-on-exit-flag proc nil)
        (set-process-filter proc #'fstar-subp-filter)
        (set-process-sentinel proc #'fstar-subp-sentinel)

  (let ((fstar-subp--lax t))
    (fstar-subp-advance-or-retract-to-point arg)))

;;;; Info queries

(defun fstar-subp--info-query (pos)
  "Prepare a header for an info query at POS."
  (format "#info <input> %S %S\n"
          (line-number-at-pos pos)
          (fstar-subp--column-number-at-pos pos)))

(defconst fstar-subp--info-response-regex
  "^(defined at \\(.+?\\)(\\([0-9]+\\),\\([0-9]+\\)-\\([0-9]+\\),\\([0-9]+\\)))")

(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 (only type information for
now) to CONTINUATION."
  (when (and success
             (eq (point) pos) ;; Point didn't move since request
             (string-match fstar-subp--info-response-regex response))
    (funcall continuation (string-trim (substring response (match-end 0))))))

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

(defun fstar-subp--eldoc-function ()
  "Issue a #info query for current point.
Results are displayed asynchronously, so this function returns
nil and the corresponding continuation calls `eldoc-message'."
  (when (fstar-subp-available-p)
    (fstar-subp--query (fstar-subp--info-query (point))
                  (apply-partially #'fstar-subp--info-continuation
                                   #'fstar-subp--eldoc-continuation (point)))
    nil))

(defun fstar-setup-eldoc ()
  "Set up eldoc support."
  (add-function :before-until (local 'eldoc-documentation-function)
                #'fstar-subp--eldoc-function)
  (eldoc-mode))

(defun fstar-teardown-eldoc ()
  "Tear down eldoc support."
  (remove-function (local 'eldoc-documentation-function)
                   #'fstar-subp--eldoc-function))

;;;; Starting the F* subprocess

(defun fstar-subp-buffer-killed ()
