      ;; 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

    "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")
  "lean keywords")

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


(require 'rx)

(defconst lean-keywords1
  '("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"
