     found))
 
 (defun fstar-find-subtype-annotation (bound)
+  "Find {...} group between point and BOUND."
   (let ((found))
     (while (and (not found) (re-search-forward "{[^:]" bound t))
       (setq found

                          (any "A-Z") (* (or wordchar (syntax symbol)))
                          symbol-end))

(defun fstar-find-id-with-type (bound)
  (fstar-find-id-maybe-type bound t))

(defun fstar-find-id-maybe-type (bound must-find-type)
  (let ((found t) (rejected t))
    (while (and found rejected)
      (setq found (re-search-forward (concat "\\(" fstar-syntax-id "\\) *\\(:\\)?") bound t))

    (indentation . "Indentation (based on control points)")
    (comments    . "Comment syntax and special comments ('(***', '(*+', etc.)")
    (flycheck    . "Real-time verification (good for small files)")
    (interactive . "Interactive verification (à la Proof-General)"))
  "Available components of F*-mode.")

(defcustom fstar-enabled-modules (mapcar #'car fstar-known-modules)
  "Which F*-mode components to load."
  :group 'fstar
  :type `(set ,@(cl-loop for (mod . desc) in fstar-known-modules
                         collect `(const :tag ,desc ,mod))))

(defun fstar-setup-hooks ()
  "Setup hooks required by F*-mode."
  (add-hook 'before-revert-hook #'fstar-subp-kill nil t))

;;;###autoload
