      ;; Types
      (,(rx word-start (or "Prop" "Type" "Type'" "Type₊" "Type₀" "Type₁" "Type₂" "Type₃") symbol-end) . 'font-lock-type-face)
      (,(rx word-start (group "Type") ".") (1 'font-lock-type-face))
-     ;; sorry
-     (,(rx word-start "sorry" word-end) . 'font-lock-warning-face)
-     (,(rx word-start "exit" word-end) . 'font-lock-warning-face)
+     ;; warnings
+     (,lean-warnings-regexp . 'font-lock-warning-face)
      ;; extra-keywords
-     (,(rx (or "∎")) . 'font-lock-keyword-face)
-     ;; lean-keywords
-     (, (concat "\\(" (regexp-opt lean-keywords 'words) "\\)")
-        (1 'font-lock-keyword-face)))))
+     (,(rx (or "∎")) . 'font-lock-keyword-face))))
 
 ;; Syntax Highlighting for Lean Info Mode
 (defconst lean-info-font-lock-defaults


(require 'rx)

(defconst lean-keywords
  '("import" "prelude" "tactic_hint" "protected" "private" "noncomputable" "definition" "renaming"
    "hiding" "exposing" "parameter" "parameters" "begin" "begin+" "proof" "qed" "conjecture" "constant" "constants"
    "hypothesis" "lemma" "corollary" "variable" "variables" "premise" "premises" "theory"

    "eval" "check" "end" "reveal" "this" "suppose"
    "using" "namespace" "section" "fields" "find_decl"
    "attribute" "local" "set_option" "extends" "include" "omit" "classes"
    "instances" "coercions" "metaclasses" "raw" "migrate" "replacing"
    "calc" "have" "show" "by" "in" "at" "let" "forall" "fun"
    "exists" "if" "dif" "then" "else" "assume" "assert" "take"
    "obtain" "from")
  "lean keywords ending with 'word' (not symbol)")
(defconst lean-keywords1-regexp
  (eval `(rx word-start (or ,@lean-keywords1) word-end)))
(defconst lean-keywords2
  '("by+")
  "lean keywords ending with 'symbol'")
(defconst lean-keywords2-regexp
  (eval `(rx word-start (or ,@lean-keywords2) symbol-end)))
(defconst lean-constants
  '("#" "@" "->" "∼" "↔" "/" "==" "=" ":=" "<->" "/\\" "\\/" "∧" "∨"
    "≠" "<" ">" "≤" "≥" "¬" "<=" ">=" "⁻¹" "⬝" "▸" "+" "*" "-" "/" "λ"
    "→" "∃" "∀")
  "lean constants")
(defconst lean-constants-regexp (regexp-opt lean-constants))
(defconst lean-modifiers
  (--map (s-concat "[" it "]")
         '("persistent" "notation" "visible" "instance" "trans-instance"
           "class" "parsing-only" "coercion" "unfold-full" "constructor"
           "reducible" "irreducible" "semireducible" "quasireducible" "wf"
           "whnf" "multiple-instances" "none" "decls" "declarations"
           "coercions" "classes" "symm" "subst" "refl" "trans" "simp" "congr"
           "notations" "abbreviations" "begin-end-hints" "tactic-hints"
           "reduce-hints" "unfold-hints" "aliases" "eqv"
           "localrefinfo"))
  "lean modifiers")
(defconst lean-modifiers-regexp
  (regexp-opt lean-modifiers))
(defconst lean-warnings '("sorry" "exit") "lean warnings")
(defconst lean-warnings-regexp (eval `(rx word-start (or ,@lean-warnings) word-end)))

(defconst lean-syntax-table
  (let ((st (make-syntax-table)))
