           (fstar-subp--column-number-at-pos pos)
           (if lax " #lax" "")))
 
-(defun fstar-subp-send-region (beg end 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."
+With non-nil LAX, send region in lax mode.  Handle results with CONTINUATION."
   (interactive "r")
-  (fstar-subp-start)
-  (let* ((body (buffer-substring-no-properties beg end))
-         (payload (fstar-subp-prepare-message body))
-         (msg (concat (fstar-subp--header beg lax) "\n" payload fstar-subp--footer)))
-    (fstar-subp-log "QUERY [%s]" msg)
-    (process-send-string fstar-subp--process msg)))
+  (let* ((payload (fstar-subp-cleanup-region (current-buffer) beg end))
+         (msg (concat (fstar-subp--push-header beg lax) "\n" payload fstar-subp--footer)))
+    (fstar-subp--query msg continuation)))
 
 (defun fstar-subp-tracking-overlay-p (overlay)
   "Return non-nil if OVERLAY is an fstar-subp tracking overlay."

        (process-put proc 'fstar-subp-source-buffer (current-buffer))
        (setq fstar-subp--process proc)))))

(defun fstar-subp-prepare-message (msg)
  "Cleanup MSG before sending it to the F* process."
  (with-temp-buffer
    (set-syntax-table fstar-syntax-table)
    (fstar-setup-comments)
    (comment-normalize-vars)
    (insert msg)
    (goto-char (point-min))
    (let (start)
      (while (setq start (comment-search-forward nil t))


(defun fstar-subp-pop-overlay (overlay)
  "Remove overlay OVERLAY and issue the corresponding #pop command."
  (fstar-assert (not fstar-subp--continuation))
  (fstar-assert (fstar-subp-live-p))
  (if (fstar-sub-overlay-contains-build-config overlay)
      (fstar-subp-kill)
    (fstar-subp--query fstar-subp--cancel nil))
  (delete-overlay overlay))

(defun fstar-subp-retract-one (overlay)
