           (fstar-subp-kill)))
        ;; Allow modifications (after retracting) in pending overlays, and in
        ;; processed overlays provided that F* isn't busy
-       ((or (not fstar-subp--busy-now)
+       ((or (not fstar-subp--continuation)
             (fstar-subp-status-eq overlay 'pending))
         (fstar-subp-retract-until (overlay-start overlay)))
        ;; Disallow modifications in processed overlays when F* is busy

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

(defun fstar-subp-kill ()


(defun fstar-subp-process-overlay (overlay)
  "Send the contents of OVERLAY to the underlying F* process."
  (fstar-assert (not fstar-subp--continuation))
  (fstar-subp-start)
  (fstar-subp-set-status overlay 'busy)
  (let ((lax (overlay-get overlay 'fstar-subp--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--continuation
    (-if-let* ((overlay (car-safe (fstar-subp-tracking-overlays 'pending))))
        (progn (fstar-subp-log "Processing queue")
               (fstar-subp-process-overlay overlay))
