 (defun fstar-subp-jump-to-issue (issue)
   "Jump to ISSUE in current buffer."
   (goto-char (fstar-issue-offset (fstar-issue-line-from issue)
-                            (fstar-issue-col-from issue))))
+                                 (fstar-issue-col-from issue))))
 
 (defun fstar-subp--local-issue-p (issue)
   "Check if ISSUE came from the current buffer."

                   status response))
          (fstar-subp-process-response status response))))))

(defun fstar-subp-clear-issues ()
  "Remove all issue overlays from current buffer."
  (cl-loop for ov being the overlays of (current-buffer)
           when (overlay-get ov 'fstar-subp-issue)
           do (delete-overlay ov)))

(defun fstar-subp-process-response (success response)
  "Process SUCCESS and RESPONSE from F* subprocess."
  (let* ((continuation fstar-subp--continuation))

     (with-current-buffer buf
       ,@body)))

;;;; Utilities

(defun fstar-in-comment-p ()
  "Return non-nil if point is inside a comment."
  (nth 4 (syntax-ppss)))

(defun fstar-in-build-config-p ()
  "Return non-nil if point is in build config comment."
  (let ((state (syntax-ppss)))
    (and (nth 4 state)
         (save-excursion
           (goto-char (nth 8 state))
           (looking-at-p (regexp-quote fstar-build-config-header))))))

;;;; Overlay classification

(defun fstar-subp-issue-overlay-p (overlay)
  "Return non-nil if OVERLAY is an fstar-subp issue overlay."
  (overlay-get overlay 'fstar-subp-issue))

(defun fstar-subp-issue-overlays ()
  "Find all -subp issues overlays in the current buffer."
  (-filter #'fstar-subp-issue-overlay-p (overlays-in (point-min) (point-max))))

(defun fstar-subp-issue-overlays-at (pt)
  "Find all -subp issues overlays at point PT."
  (-filter #'fstar-subp-issue-overlay-p (overlays-at pt t)))

(defun fstar-subp-tracking-overlay-p (overlay)
  "Return non-nil if OVERLAY is an fstar-subp tracking overlay."
  (fstar-subp-status overlay))

(defun fstar-subp-tracking-overlays (&optional status)
  "Find all -subp tracking overlays with status STATUS in the current buffer.

If STATUS is nil, return all fstar-subp overlays."
  (sort (cl-loop for overlay being the overlays of (current-buffer)
                 when (fstar-subp-tracking-overlay-p overlay)
                 when (or (not status) (fstar-subp-status-eq overlay status))
                 collect overlay)
        (lambda (o1 o2) (< (overlay-start o1) (overlay-start o2)))))

(defun fstar-subp-remove-tracking-overlays ()
  "Remove all F* overlays in the current buffer."
  (mapcar #'delete-overlay (fstar-subp-tracking-overlays)))

(defun fstar-subp-remove-issues-overlays ()
  "Remove all F* overlays in the current buffer."
  (mapcar #'delete-overlay (fstar-subp-issue-overlays)))

;;;; Basic subprocess operations

(defun fstar-subp-live-p (&optional proc)
  "Return t if the PROC is a live F* subprocess.
If PROC is nil, use the current buffer's `fstar-subp--process'."
  (setq proc (or proc fstar-subp--process))
  (and proc (process-live-p proc)))


(defun fstar-subp--query (query continuation)
  "Send QUERY to F* subprocess; handle results with CONTINUATION."
  (fstar-subp-log "QUERY [%s]" query)
  (fstar-assert (not fstar-subp--continuation))
  (setq fstar-subp--continuation continuation)
  (fstar-subp-start)
  (process-send-string fstar-subp--process query))

(defun fstar-subp-find-response (proc)
  "Find full response in PROC's buffer; handle it if found."
