diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el
index d59270afbf..72909bd33a 100644
--- a/src/emacs/lean-mode.el
+++ b/src/emacs/lean-mode.el
@@ -15,6 +15,7 @@
 (require 'lean-input)
 (require 'lean-type)
 (require 'lean-tags)
+(require 'lean-syntax)
 
 (defun lean-compile-string (exe-name args file-name)
   "Concatenate exe-name, args, and file-name"
@@ -53,63 +54,51 @@
   (local-set-key "\M-."     'lean-find-tag)
   (local-set-key [tab]      'lean-complete-tag))
 
-(define-abbrev-table 'lean-mode-abbrev-table '(
-    ("var"    "variable")
+(define-abbrev-table 'lean-abbrev-table
+  '(("var"    "variable")
     ("vars"   "variables")
     ("def"    "definition")
     ("th"     "theorem")))
 
-(define-generic-mode
-    'lean-mode     ;; name of the mode to create
-  '("--")          ;; comments start with
-  '("import" "abbreviation" "opaque_hint" "tactic_hint" "definition" "renaming" "inline" "hiding" "exposing" "parameter" "parameters" "proof" "qed" "conjecture" "hypothesis" "lemma" "corollary" "variable" "variables" "print" "theorem" "axiom" "inductive" "with" "structure" "universe" "alias" "help" "environment" "options" "precedence" "postfix" "prefix" "calc_trans" "calc_subst" "calc_refl" "infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end" "private" "using" "namespace" "builtin" "including" "instance" "section" "set_option" "add_rewrite" "extends") ;; some keywords
-  '(("\\_<\\(bool\\|int\\|nat\\|real\\|Prop\\|Type\\|ℕ\\|ℤ\\)\\_>" . 'font-lock-type-face)
-    ("\\_<\\(calc\\|have\\|obtains\\|show\\|by\\|in\\|let\\|forall\\|fun\\|exists\\|if\\|then\\|else\\|assume\\|take\\|obtain\\|from\\)\\_>" . font-lock-keyword-face)
-    ("\"[^\"]*\"" . 'font-lock-string-face)
-    ("\\(->\\|↔\\|/\\\\\\|==\\|\\\\/\\|[*+/<=>¬∧∨≠≤≥-]\\)" . 'font-lock-constant-face)
-    ("\\(λ\\|→\\|∃\\|∀\\|:\\|:=\\)" . font-lock-constant-face)
-    ("\\_<\\(\\b.*_tac\\|Cond\\|or_else\\|t\\(?:hen\\|ry\\)\\|when\\|assumption\\|apply\\|b\\(?:ack\\|eta\\)\\|done\\|exact\\)\\_>" . 'font-lock-constant-face)
-    ("\\_<\\(universe\\|inductive\\|theorem\\|axiom\\|lemma\\|hypothesis\\|abbreviation\\|definition\\|variable\\|parameter\\)\\_>[ \t\{\[]*\\([^ \t\n]*\\)" (2 'font-lock-function-name-face))
-    ("\\_<\\(variables\\|parameters\\)\\_>[ \t\(\{\[]*\\([^:]*\\)" (2 'font-lock-function-name-face))
-    ("\\(set_opaque\\|set_option\\)[ \t]*\\([^ \t\n]*\\)" (2 'font-lock-constant-face))
-    ("\\_<_\\_>" . 'font-lock-preprocessor-face)
-    ("\\_<sorry\\_>" . 'font-lock-warning-face)
-    ;;
-    )
-  '("\\.lean$")                    ;; files for which to activate this mode
-  '((lambda()
-      (set-input-method "Lean")
-      (set (make-local-variable 'lisp-indent-function)
-           'common-lisp-indent-function)
-      (lean-set-keys)
-      (setq local-abbrev-table lean-mode-abbrev-table)
-      (abbrev-mode 1)
-      (add-hook 'before-change-functions '
-                lean-before-change-function nil t)
-      (add-hook 'after-change-functions '
-                lean-after-change-function nil t)
-      ;; Draw a vertical line for rule-column
-      (when (and lean-rule-column
-                 lean-show-rule-column-method)
-        (cl-case lean-show-rule-column-method
-          ('vline (require 'fill-column-indicator)
-                  (setq fci-rule-column lean-rule-column)
-                  (setq fci-rule-color lean-rule-color)
-                  (add-hook 'lean-mode-hook 'fci-mode nil t))))
-      ;; Delete Trailing Whitespace
-      (if lean-delete-trailing-whitespace
-          (progn (require 'whitespace-cleanup-mode)
-                 (add-hook 'lean-mode-hook 'whitespace-cleanup-mode nil t))
-        (remove-hook 'lean-mode-hook 'whitespace-cleanup-mode))
-      ;; eldoc
-      (set (make-local-variable 'eldoc-documentation-function)
-           'lean-eldoc-documentation-function)
-      (eldoc-mode +1)
-      ))
-  "A mode for Lean files"          ;; doc string for this mode
-  )
+;; Automode List
+;;;###autoload
+(define-derived-mode lean-mode prog-mode "Lean"
+  "Major mode for Lean"
+  :syntax-table lean-syntax-table
+  :abbrev-table lean-abbrev-table
+  :group 'lean
+  (set (make-local-variable 'comment-start) "--")
+  (set (make-local-variable 'font-lock-defaults) lean-font-lock-defaults)
+  (set (make-local-variable 'indent-tabs-mode) nil)
+  (set-input-method "Lean")
+  (set (make-local-variable 'lisp-indent-function)
+       'common-lisp-indent-function)
+  (lean-set-keys)
+  (abbrev-mode 1)
+  (add-hook 'before-change-functions 'lean-before-change-function nil t)
+  (add-hook 'after-change-functions 'lean-after-change-function nil t)
+  ;; Draw a vertical line for rule-column
+  (when (and lean-rule-column
+             lean-show-rule-column-method)
+    (cl-case lean-show-rule-column-method
+      ('vline (require 'fill-column-indicator)
+              (setq fci-rule-column lean-rule-column)
+              (setq fci-rule-color lean-rule-color)
+              (add-hook 'lean-mode-hook 'fci-mode nil t))))
+  ;; Delete Trailing Whitespace
+  (if lean-delete-trailing-whitespace
+      (progn (require 'whitespace-cleanup-mode)
+             (add-hook 'lean-mode-hook 'whitespace-cleanup-mode nil t))
+    (remove-hook 'lean-mode-hook 'whitespace-cleanup-mode))
+  ;; eldoc
+  (set (make-local-variable 'eldoc-documentation-function)
+       'lean-eldoc-documentation-function))
+
+;; Automatically use lean-mode for .lean files.
+;;;###autoload
+(push '("\\.lean$" . lean-mode) auto-mode-alist)
+;; Use utf-8 encoding
+;;;###autoload
+(modify-coding-system-alist 'file "\\.lean\\'" 'utf-8)
+
 (provide 'lean-mode)
-; (regexp-opt '("Int" "Bool" "Nat" "Type" "Real") t)
-; (regexp-opt '("let" "in" "have" "calc" "forall" "exists") t)
-; (regexp-opt '("=" "->" "≠" "∨" "∧" "¬" "/\\" "\\/" "+" "-" "*" "/" "<" ">" "≤" "≥" "==" "∀" "∃" "→" "λ" ":") t)
-; (regexp-opt '("apply" "exact" "trivial" "absurd" "beta" "apply" "unfold" "done" "back" "Try" "Then" "OrElse" "OrElse" "Cond" "When" "unfold_all" ) t)
diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el
new file mode 100644
index 0000000000..0edbe05e1f
--- /dev/null
+++ b/src/emacs/lean-syntax.el
@@ -0,0 +1,88 @@
+;; Copyright (c) 2013, 2014 Microsoft Corporation. All rights reserved.
+;; Released under Apache 2.0 license as described in the file LICENSE.
+;;
+;; Author: Leonardo de Moura
+;;         Soonho Kong
+;;
+
+(require 'rx)
+
+(defconst lean-keywords
+  '("import" "abbreviation" "opaque_hint" "tactic_hint" "definition" "renaming"
+    "inline" "hiding" "exposing" "parameter" "parameters" "proof" "qed" "conjecture"
+    "hypothesis" "lemma" "corollary" "variable" "variables" "print" "theorem"
+    "axiom" "inductive" "with" "structure" "universe" "alias" "help" "environment"
+    "options" "precedence" "postfix" "prefix" "calc_trans" "calc_subst" "calc_refl"
+    "infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end"
+    "private" "using" "namespace" "builtin" "including" "instance" "section"
+    "set_option" "add_rewrite" "extends")
+  "lean keywords")
+
+(defconst lean-syntax-table
+  (let ((st (make-syntax-table (standard-syntax-table))))
+    ;; Matching parens
+    (modify-syntax-entry ?\( "()" st)
+    (modify-syntax-entry ?\) ")(" st)
+    (modify-syntax-entry ?\[ "(]" st)
+    (modify-syntax-entry ?\] ")[" st)
+
+    ;; Matching {}, but with nested comments
+    (modify-syntax-entry ?\{ "(} 1bn" st)
+    (modify-syntax-entry ?\} "){ 4bn" st)
+    (modify-syntax-entry ?\- "_ 123" st)
+    (modify-syntax-entry ?\n ">" st)
+
+    ;; ' and _ can be names
+    (modify-syntax-entry ?' "w" st)
+    (modify-syntax-entry ?_ "w" st)
+
+    ;; Lean operator chars
+    (mapc #'(lambda (ch) (modify-syntax-entry ch "_" st))
+          "!#$%&*+./<=>@^|~:")
+
+    ;; Whitespace is whitespace
+    (modify-syntax-entry ?\  " " st)
+    (modify-syntax-entry ?\t " " st)
+
+    ;; ;; Strings
+    (modify-syntax-entry ?\" "\"" st)
+    (modify-syntax-entry ?\\ "/" st)
+    st))
+
+(defconst lean-font-lock-defaults
+  `((;; Comments
+     (,(rx (group "--") (group (0+ ".")))
+      (1 font-lock-comment-delimiter-face)
+      (2 font-lock-comment-face))
+     ;; Types
+     (,(rx symbol-start (or "bool" "int" "nat" "real" "Prop" "Type" "ℕ" "ℤ") symbol-end) . 'font-lock-type-face)
+     ;; Keywords
+     (,(rx symbol-start (or "calc" "have" "obtains" "show" "by" "in" "let" "forall" "fun"
+                            "exists" "if" "then" "else" "assume" "take" "obtain" "from") symbol-end)
+      . font-lock-keyword-face)
+     ;; String
+     ("\"[^\"]*\"" . 'font-lock-string-face)
+     ;; Constants
+     (,(rx (or "->" "↔" "/" "==" "\/" "[*+/<=>¬∧∨≠≤≥-]")) . 'font-lock-constant-face)
+     (,(rx (or "λ" "→" "∃" "∀" ":" ":=")) . 'font-lock-constant-face )
+     (,(rx symbol-start
+           (or "\\b.*_tac" "Cond" "or_else" "then" "try" "when" "assumption" "apply" "back" "beta" "done" "exact")
+           symbol-end)
+      . 'font-lock-constant-face)
+     ;; universe/inductive/theorem... "names"
+     (,(rx symbol-start
+            (group (or "universe" "inductive" "theorem" "axiom" "lemma" "hypothesis"
+                       "abbreviation" "definition" "variable" "parameter"))
+            symbol-end
+            (zero-or-more (or whitespace "{" "["))
+            (group (zero-or-more (not whitespace))))
+        (2 'font-lock-function-name-face))
+     ("\\(set_opaque\\|set_option\\)[ \t]*\\([^ \t\n]*\\)" (2 'font-lock-constant-face))
+     ;; place holder
+     (,(rx symbol-start "_" symbol-end) . 'font-lock-preprocessor-face)
+     ;; sorry
+     (,(rx symbol-start "sorry" symbol-end) . 'font-lock-warning-face)
+     ;; lean-keywords
+     (, (concat "\\(" (regexp-opt lean-keywords 'words) "\\)")
+        (1 'font-lock-keyword-face)))))
+(provide 'lean-syntax)