From 27ad84664101be9fd1a19047268a95f24ba6800c Mon Sep 17 00:00:00 2001
From: Soonho Kong <soonhok@cs.cmu.edu>
Date: Tue, 24 Feb 2015 13:21:40 -0500
Subject: [PATCH] highlight names followed nameProviders in lean-mode

---
 lib/ace/mode/lean_highlight_rules.js | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/lib/ace/mode/lean_highlight_rules.js b/lib/ace/mode/lean_highlight_rules.js
index 4ba9d484..06669de3 100644
--- a/lib/ace/mode/lean_highlight_rules.js
+++ b/lib/ace/mode/lean_highlight_rules.js
@@ -53,6 +53,9 @@ var leanHighlightRules = function() {
           "universes", "using", "variable", "variables", "with"].join("|")
     );
 
+    var nameProviders = (
+        ["inductive", "structure", "record", "theorem", "axiom",
+         "axioms", "lemma", "hypothesis", "definition", "constant"].join("|")
     );
 
     var storageType = (
@@ -109,6 +112,8 @@ var leanHighlightRules = function() {
                     {defaultToken: "string"}
                 ]
             }, {
+                token : "keyword.control", regex : nameProviders, next : [
+                    {token : "variable.language", regex : identifierRe, next : "start"} ]
             }, {
                 token : "constant.numeric", // hex
                 regex : "0[xX][0-9a-fA-F]+(L|l|UL|ul|u|U|F|f|ll|LL|ull|ULL)?\\b"