 ;;; Prettify symbols
 
 (defcustom fstar-symbols-alist '(("exists" . ?∃) ("forall" . ?∀) ("fun" . ?λ)
-                            ("nat" . ?ℕ) ("int" . ?ℤ)
-                            ("True" . ?⊤) ("False" . ?⊥)
-                            ("*" . ?×) ("~>" . ?↝)
-                            ("<=" . ?≤) (">=" . ?≥) ("::" . ?⸬)
-                            ("/\\" . ?∧) ("\\/" . ?∨) ("~" . ?¬) ("<>" . ?≠)
-                            ;; ("&&" . ?∧) ("||" . ?∨) ("=!=" . ?≠)
-                            ("<==>" . ?⟺) ("==>" . ?⟹)
-                            ("=>" . ?⇒) ("->" . ?→)
-                            ;; ("(|" . 10629) ("|)" . 10630)
-                            ("'a" . ?α) ("'b" . ?β) ("'c" . ?γ)
-                            ("'d" . ?δ) ("'e" . ?ϵ))
+                                 ("nat" . ?ℕ) ("int" . ?ℤ)
+                                 ("True" . ?⊤) ("False" . ?⊥)
+                                 ("*" . ?×) ("~>" . ?↝)
+                                 ("<=" . ?≤) (">=" . ?≥) ("::" . ?⸬)
+                                 ("/\\" . ?∧) ("\\/" . ?∨) ("~" . ?¬) ("<>" . ?≠)
+                                 ;; ("&&" . ?∧) ("||" . ?∨) ("=!=" . ?≠)
+                                 ("<==>" . ?⟺) ("==>" . ?⟹)
+                                 ("=>" . ?⇒) ("->" . ?→)
+                                 ;; ("(|" . 10629) ("|)" . 10630)
+                                 ("'a" . ?α) ("'b" . ?β) ("'c" . ?γ)
+                                 ("'d" . ?δ) ("'e" . ?ϵ))
   "Fstar symbols."
   :group 'fstar
   :type 'alist)

          (fstar-subp--column-number-at-pos pos)
          (if lax " #lax" "")))

(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-send-region (beg end lax continuation)
  "Send the region between BEG and END to the inferior F* process.
With non-nil LAX, send region in lax mode.  Handle results with 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."
