   (let* ((payload (fstar-subp--clean-buffer-substring beg end)))
     (fstar-subp--query (fstar-subp--peek-query beg kind payload) continuation)))
 
-(defun fstar-subp-overlay-attempt-modification (overlay &rest _args)
+(defun fstar-subp-overlay-attempt-modification (overlay _is-before _beg _end &optional _pre-length)
   "Allow or prevent attempts to modify OVERLAY.
 
-Modifications are only allowed if it is safe to retract up to the beginning of the current overlay."
+Modifications are only allowed if it is safe to retract up to the
+beginning of the current overlay."
   (let ((inhibit-modification-hooks t))
     (when (overlay-buffer overlay) ;; Hooks can be called multiple times
       (cond

                 (fstar-subp-process-overlay overlay))
        (fstar-log 'info "Queue is empty (%d overlays)" (length (fstar-subp-tracking-overlays)))))))

;;; ;; Advancing and retracting

(defun fstar-subp-unprocessed-beginning ()
  "Find the beginning of the unprocessed buffer area."
  (or (cl-loop for overlay in (fstar-subp-tracking-overlays)
               maximize (overlay-end overlay))
      (point-min)))

(defun fstar-skip-spaces-backwards-from (point)
  "Go to POINT, skip spaces backwards, and return position."
  (save-excursion
    (goto-char point)
    (skip-chars-backward "\n\r\t ")
    (point)))

(defun fstar-subp-enqueue-until (end &optional no-error)
  "Mark region up to END busy, and enqueue the newly created overlay.

If NO-ERROR is set, do not report an error if the region is empty."
  (fstar-subp-start)
  (let ((beg (fstar-subp-unprocessed-beginning))
        (end (fstar-skip-spaces-backwards-from end)))
    (when (eq (char-after end) ?\n)
      (cl-incf end))
    (fstar-assert (cl-loop for overlay in (overlays-in beg end)
                      never (fstar-subp-tracking-overlay-p overlay)))
    (if (<= end beg)
        (unless no-error
          (user-error "Nothing more to process!"))
      (let ((overlay (make-overlay beg end (current-buffer) nil nil)))
        (fstar-subp-remove-orphaned-issue-overlays (point-min) (point-max))
        (overlay-put overlay 'fstar-subp--lax fstar-subp--lax)
        (fstar-subp-set-status overlay 'pending)
        (fstar-subp--set-queue-timer)))))

(defcustom fstar-subp-block-sep
  (concat "\\(?:\\'\\|\n\\(?:[[:space:]]*\n\\)+"
          "\\(?:" fstar-syntax-block-start-re
          "\\|" fstar-comment-start-skip "\\)\\)")
  "Regular expression used when looking for source blocks."
  :group 'fstar
  :type 'string
  :safe #'stringp)

(defun fstar-subp-skip-comments-and-whitespace ()
  "Skip over comments and whitespace."
  (while (or (> (skip-chars-forward " \r\n\t") 0)
             (comment-forward 1))))

(defun fstar-subp-next-block-sep (bound)
  "Find the next block separator before BOUND.
Ignores separators found in comments."
  (let (pos)
    (save-excursion
      (while (and (null pos) (re-search-forward fstar-subp-block-sep bound t))
        (goto-char (point-at-bol))
        (unless (fstar-in-comment-p)
          (setq pos (point)))))
    (when pos
      (goto-char pos))))

(defun fstar-subp--next-unprocessed-start (n)
  "Find the start of the at most (N + 1)th unprocessed block."
  (save-excursion
    (goto-char (fstar-subp-unprocessed-beginning))
    (dotimes (_ n)
      (fstar-subp-skip-comments-and-whitespace)
      (fstar-subp-next-block-sep nil))
    (point)))

(defun fstar-subp-goto-beginning-of-unprocessed ()
  "Go to beginning of unprocessed region."
  (interactive)
  (goto-char (fstar-subp-unprocessed-beginning)))

(defun fstar-subp-advance-next ()
  "Process buffer until `fstar-subp-block-sep'."
  (interactive)
  (fstar-subp-start)
  (-if-let* ((next-start (fstar-subp--next-unprocessed-start 1)))
      (fstar-subp-enqueue-until (goto-char next-start))
    (user-error "Cannot find a full block to process")))

(defun fstar-subp-pop-overlay (overlay)

(defun fstar--indentation-previous-line ()
  "Go to previous non-blank line."
  (goto-char (point-at-bol))
  (skip-chars-backward fstar--spaces))

(defun fstar--indentation-points-before (&optional max-column)
  "Add indentation points before MAX-COLUMN or current point to POINTS."
