              (2 'font-lock-function-name-face append)
              (3 'fstar-attribute-face append)))
       ("%\\[" ("%\\[\\([^]]+\\)\\]"
-              (fstar-group-pre-matcher 1 0) nil
-              (1 'fstar-decreases-face append)))
+               (fstar-group-pre-matcher 1 0) nil
+               (1 'fstar-decreases-face append)))
       (,(concat "\\_<\\(let\\(?: +rec\\)?\\)\\(\\(?: +" id "\\)?\\) +[^=]+=")
        (1 'fstar-structure-face)
        (2 'font-lock-function-name-face)

      (fstar-subp-kill)
      (error "Invalid state: Received output, but no region was busy"))
    (setq fstar-subp--busy-now nil)
    (pcase status
      (`t   (fstar-subp-handle-success response overlay))
      (`nil (fstar-subp-handle-failure response overlay))

  (when (not (process-live-p proc))
    (fstar-subp-killed proc)))

(defun fstar-subp-remove-tracking-overlays ()
  "Remove all F* overlays in the current buffer."
  (mapcar #'delete-overlay (fstar-subp-tracking-overlays)))

(defun fstar-subp-remove-issues-overlays ()
  "Remove all F* overlays in the current buffer."
  (mapcar #'delete-overlay (fstar-subp-issues-overlays)))

(defmacro fstar-subp-with-process-buffer (proc &rest body)
  "Move to PROC's buffer to eval BODY."
