 
 (defun fstar-subp-process-overlay (overlay)
   "Send the contents of OVERLAY to the underlying F* process."
-  (fstar-assert (not fstar-subp--busy-now))
+  (fstar-assert (not fstar-subp--continuation))
   (fstar-subp-start)
   (fstar-subp-set-status overlay 'busy)
-  (setq fstar-subp--busy-now overlay)
   (let ((lax (overlay-get overlay 'fstar-subp--lax)))
-    (fstar-subp-send-region (overlay-start overlay) (overlay-end overlay) lax)))
+    (fstar-subp-send-region (overlay-start overlay) (overlay-end overlay) lax
+                       (apply-partially #'fstar-subp--overlay-continuation overlay))))
 
 (defun fstar-subp-process-queue ()
   "Process the next pending overlay, if any."
   (fstar-subp-start)
-  (unless fstar-subp--busy-now
+  (unless fstar-subp--continuation
     (-if-let* ((overlay (car-safe (fstar-subp-tracking-overlays 'pending))))
         (progn (fstar-subp-log "Processing queue")
                (fstar-subp-process-overlay 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))

    (kill-buffer))
  (fstar-subp-remove-tracking-overlays)
  (fstar-subp-remove-issues-overlays)
  (setq fstar-subp--continuation nil
        fstar-subp--process nil))

(defun fstar-subp-kill ()
