 (defun fstar-subp-advance-next ()
   "Process buffer until `fstar-subp-block-sep'."
   (interactive)
+  (fstar-subp-start)
   (goto-char (fstar-subp-unprocessed-beginning))
   (fstar-subp-skip-comments-and-whitespace)
   (-if-let* ((next-start (re-search-forward fstar-subp-block-sep nil t)))

(defun fstar-subp-filter (proc string)
  "Handle PROC's output (STRING)."
  (when string
    (fstar-subp-log "OUTPUT [%s]" (replace-regexp-in-string "\n" " // " string t t))
    (fstar-subp-with-process-buffer proc
      (goto-char (point-max))
      (insert string)

    (accept-process-output fstar-subp--process 0.25 nil t))
  (fstar-subp-killed fstar-subp--process))

(defun fstar-subp-sentinel (proc signal)
  "Hamdle signals from PROC."
  (fstar-subp-log "SENTINEL [%s] [%s]" signal (process-status proc))
  (when (or (memq (process-status proc) '(exit signal))
	    (not (process-live-p proc)))
    (fstar-subp-killed proc)))

(defun fstar-subp-remove-tracking-overlays ()
