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


(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)))


(defun fstar-subp--ensure-available (error-fn)
  "Raise an error with ERROR-FN if F* isn't available."
  (when (fstar-subp--busy-p)
    (funcall error-fn "F* seems busy; please wait until processing is complete"))
  (unless (fstar-subp-live-p)
    (funcall error-fn "Please start F* before jumping to a definition")))
