 ;;; Prettify symbols
 
 (defcustom fstar-symbols-alist '(("exists" . ?∃) ("forall" . ?∀) ("fun" . ?λ)
-                                 ("nat" . ?ℕ) ("int" . ?ℤ)
-                                 ("True" . ?⊤) ("False" . ?⊥)
-                                 ("*" . ?×) ("~>" . ?↝)
-                                 ("<=" . ?≤) (">=" . ?≥) ("::" . ?⸬)
-                                 ("/\\" . ?∧) ("\\/" . ?∨) ("~" . ?¬) ("<>" . ?≠)
-                                 ;; ("&&" . ?∧) ("||" . ?∨) ("=!=" . ?≠)
-                                 ("<==>" . ?⟺) ("==>" . ?⟹)
-                                 ("=>" . ?⇒) ("->" . ?→)
-                                 ;; ("(|" . 10629) ("|)" . 10630)
-                                 ("'a" . ?α) ("'b" . ?β) ("'c" . ?γ)
-                                 ("'d" . ?δ) ("'e" . ?ϵ))
+                            ("nat" . ?ℕ) ("int" . ?ℤ)
+                            ("True" . ?⊤) ("False" . ?⊥)
+                            ("*" . ?×) ("~>" . ?↝)
+                            ("<=" . ?≤) (">=" . ?≥) ("::" . ?⸬)
+                            ("/\\" . ?∧) ("\\/" . ?∨) ("~" . ?¬) ("<>" . ?≠)
+                            ;; ("&&" . ?∧) ("||" . ?∨) ("=!=" . ?≠)
+                            ("<==>" . ?⟺) ("==>" . ?⟹)
+                            ("=>" . ?⇒) ("->" . ?→)
+                            ;; ("(|" . 10629) ("|)" . 10630)
+                            ("'a" . ?α) ("'b" . ?β) ("'c" . ?γ)
+                            ("'d" . ?δ) ("'e" . ?ϵ))
   "Fstar symbols."
   :group 'fstar
   :type 'alist)

  (match-end (or bound-to 0)))

(defconst fstar-syntax-id-unwrapped (rx (? (or "#" "'"))
                                        (any "a-z_") (* (or wordchar (syntax symbol)))
                                        (? "." (* (or wordchar (syntax symbol))))))

(defconst fstar-syntax-id (concat "\\_<" fstar-syntax-id-unwrapped "\\_>"))

(defconst fstar-syntax-cs (rx symbol-start
                              (any "A-Z") (* (or wordchar (syntax symbol)))
                              symbol-end))

(defconst fstar-syntax-universe-id-unwrapped (rx "'u" (* (or wordchar (syntax symbol)))))

(defconst fstar-syntax-universe-id (concat "\\_<" fstar-syntax-universe-id-unwrapped "\\_>"))

(defconst fstar-syntax-universe (concat "\\(" fstar-syntax-universe-id
                                        "\\|u#([^)]*)\\)"))

(defconst fstar-syntax-ids (concat "\\(" fstar-syntax-id "\\(?: +" fstar-syntax-id "\\)*\\)"))


  (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 (buffer)
  "Process the next pending overlay of BUFFER, if any."
