From 3c34a9852f54637106a7888ef99e329e82ecd051 Mon Sep 17 00:00:00 2001
From: Soonho Kong <soonhok@cs.cmu.edu>
Date: Tue, 24 Feb 2015 13:20:28 -0500
Subject: [PATCH] add and sort keywords/storage-modifiers for lean-mode

---
 lib/ace/mode/lean_highlight_rules.js | 37 +++++++++++++++-------------
 1 file changed, 20 insertions(+), 17 deletions(-)

diff --git a/lib/ace/mode/lean_highlight_rules.js b/lib/ace/mode/lean_highlight_rules.js
index f653096b..91440169 100644
--- a/lib/ace/mode/lean_highlight_rules.js
+++ b/lib/ace/mode/lean_highlight_rules.js
@@ -38,20 +38,21 @@ var TextHighlightRules = require("./text_highlight_rules").TextHighlightRules;
 var leanHighlightRules = function() {
 
     var keywordControls = (
-        ["import", "tactic_hint", "protected", "find_decl",
-         "private", "opaque", "definition", "renaming", "hiding", "exposing",
-         "parameter", "parameters", "begin", "proof", "qed", "conjecture", "premise", "premises",
-         "constant", "constants", "example", "attribute", "local",
-         "hypothesis", "lemma", "corollary", "variable", "variables", "print",
-         "theorem", "context", "open", "as", "export", "axiom", "inductive",
-         "with", "structure", "record", "universe", "universes", "alias", "help", "environment",
-         "options", "precedence", "postfix", "prefix", "calc_trans",
-         "calc_subst", "calc_refl", "infix", "infixl", "infixr", "notation",
-         "eval", "check", "exit", "end", "using", "namespace",
-         "section", "set_option", "omit", "classes", "instances", "coercions", "raw",
-         "add_rewrite", "extends", "calc", "have", "obtains", "show", "by", "in", "let",
-         "forall", "fun", "exists", "if", "then", "else", "assume", "match",
-         "take", "obtain", "from", "axioms", "fields"].join("|")
+        [ "add_rewrite", "alias", "as", "assume", "attribute",
+          "begin", "by", "calc", "calc_refl", "calc_subst", "calc_trans", "check",
+          "classes", "coercions", "conjecture", "constants", "context",
+          "corollary", "else", "end", "environment", "eval", "example",
+          "exists", "exit", "export", "exposing", "extends", "fields", "find_decl",
+          "forall", "from", "fun", "have", "help", "hiding", "if",
+          "import", "in", "infix", "infixl", "infixr", "instances",
+          "let", "local", "match", "namespace", "notation", "obtain", "obtains",
+          "omit", "opaque", "open", "options", "parameter", "parameters", "postfix",
+          "precedence", "prefix", "premise", "premises", "print", "private", "proof",
+          "protected", "qed", "raw", "renaming", "section", "set_option",
+          "show", "tactic_hint", "take", "then", "universe",
+          "universes", "using", "variable", "variables", "with"].join("|")
+    );
+
     );
 
     var storageType = (
@@ -60,9 +61,11 @@ var leanHighlightRules = function() {
 
     var storageModifiers = (
         "\\[(" +
-            ["persistent", "notation", "parsing-only", "visible", "instance", "class", "prefix", "axioms", "fields",
-             "multiple-instances", "classes", "instances", "coercions", "options", "trust",
-             "coercion", "reducible", "irreducible", "raw"].join("|") +
+            ["abbreviations", "all-transparent", "begin-end-hints", "class", "classes", "coercion",
+             "coercions", "declarations", "decls", "instance", "irreducible",
+             "multiple-instances", "notation", "notations", "parsing-only", "persistent",
+             "reduce-hints", "reducible", "tactic-hints", "visible", "wf", "whnf"
+            ].join("|") +
             ")\\]"
     );