From b3da9336eed368b5a23bb86b731caee1b43768cd Mon Sep 17 00:00:00 2001
From: Soonho Kong <soonhok@cs.cmu.edu>
Date: Mon, 23 Feb 2015 07:01:43 -0500
Subject: [PATCH 1/9] add 'lean' mode for Lean Theorem Prover files

---
 lib/ace/ext/modelist.js              |   2 +-
 lib/ace/mode/lean.js                 | 101 ++++++++++++
 lib/ace/mode/lean_highlight_rules.js | 224 +++++++++++++++++++++++++++
 lib/ace/snippets/lean.js             |   7 +
 lib/ace/snippets/lean.snippets       |   0
 5 files changed, 333 insertions(+), 1 deletion(-)
 create mode 100644 lib/ace/mode/lean.js
 create mode 100644 lib/ace/mode/lean_highlight_rules.js
 create mode 100644 lib/ace/snippets/lean.js
 create mode 100644 lib/ace/snippets/lean.snippets

diff --git a/lib/ace/ext/modelist.js b/lib/ace/ext/modelist.js
index 69aa8972..fba3a245 100644
--- a/lib/ace/ext/modelist.js
+++ b/lib/ace/ext/modelist.js
@@ -99,6 +99,7 @@ var supportedModes = {
     JSX:         ["jsx"],
     Julia:       ["jl"],
     LaTeX:       ["tex|latex|ltx|bib"],
+    Lean:        ["lean|hlean"],
     LESS:        ["less"],
     Liquid:      ["liquid"],
     Lisp:        ["lisp"],
@@ -192,4 +193,3 @@ module.exports = {
 };
 
 });
-
diff --git a/lib/ace/mode/lean.js b/lib/ace/mode/lean.js
new file mode 100644
index 00000000..e421f2b5
--- /dev/null
+++ b/lib/ace/mode/lean.js
@@ -0,0 +1,101 @@
+/* ***** BEGIN LICENSE BLOCK *****
+ * Distributed under the BSD license:
+ *
+ * Copyright (c) 2010, Ajax.org B.V.
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *     * Redistributions of source code must retain the above copyright
+ *       notice, this list of conditions and the following disclaimer.
+ *     * Redistributions in binary form must reproduce the above copyright
+ *       notice, this list of conditions and the following disclaimer in the
+ *       documentation and/or other materials provided with the distribution.
+ *     * Neither the name of Ajax.org B.V. nor the
+ *       names of its contributors may be used to endorse or promote products
+ *       derived from this software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
+ * ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
+ * WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+ * DISCLAIMED. IN NO EVENT SHALL AJAX.ORG B.V. BE LIABLE FOR ANY
+ * DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
+ * (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
+ * LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
+ * ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+ * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+ * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ *
+ * ***** END LICENSE BLOCK ***** */
+
+define(function(require, exports, module) {
+"use strict";
+
+var oop = require("../lib/oop");
+var TextMode = require("./text").Mode;
+var leanHighlightRules = require("./lean_highlight_rules").leanHighlightRules;
+var MatchingBraceOutdent = require("./matching_brace_outdent").MatchingBraceOutdent;
+var Range = require("../range").Range;
+// TODO(soonhok): figure out behavior and foldmode
+// var CstyleBehaviour = require("./behaviour/cstyle").CstyleBehaviour;
+// var CStyleFoldMode = require("./folding/cstyle").FoldMode;
+
+var Mode = function() {
+    this.HighlightRules = leanHighlightRules;
+
+    this.$outdent = new MatchingBraceOutdent();
+    // this.$behaviour = new CstyleBehaviour();
+    // this.foldingRules = new CStyleFoldMode();
+};
+oop.inherits(Mode, TextMode);
+
+(function() {
+
+    this.lineCommentStart = "--";
+    this.blockComment = {start: "/-", end: "-/"};
+
+    this.getNextLineIndent = function(state, line, tab) {
+        var indent = this.$getIndent(line);
+
+        var tokenizedLine = this.getTokenizer().getLineTokens(line, state);
+        var tokens = tokenizedLine.tokens;
+        var endState = tokenizedLine.state;
+
+        if (tokens.length && tokens[tokens.length-1].type == "comment") {
+            return indent;
+        }
+
+        if (state == "start") {
+            var match = line.match(/^.*[\{\(\[]\s*$/);
+            if (match) {
+                indent += tab;
+            }
+        } else if (state == "doc-start") {
+            if (endState == "start") {
+                return "";
+            }
+            var match = line.match(/^\s*(\/?)\*/);
+            if (match) {
+                if (match[1]) {
+                    indent += " ";
+                }
+                indent += "- ";
+            }
+        }
+
+        return indent;
+    };
+
+    this.checkOutdent = function(state, line, input) {
+        return this.$outdent.checkOutdent(line, input);
+    };
+
+    this.autoOutdent = function(state, doc, row) {
+        this.$outdent.autoOutdent(doc, row);
+    };
+
+    this.$id = "ace/mode/lean";
+}).call(Mode.prototype);
+
+exports.Mode = Mode;
+});
diff --git a/lib/ace/mode/lean_highlight_rules.js b/lib/ace/mode/lean_highlight_rules.js
new file mode 100644
index 00000000..d5f9a67c
--- /dev/null
+++ b/lib/ace/mode/lean_highlight_rules.js
@@ -0,0 +1,224 @@
+/* ***** BEGIN LICENSE BLOCK *****
+ * Distributed under the BSD license:
+ *
+ * Copyright (c) 2010, Ajax.org B.V.
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *     * Redistributions of source code must retain the above copyright
+ *       notice, this list of conditions and the following disclaimer.
+ *     * Redistributions in binary form must reproduce the above copyright
+ *       notice, this list of conditions and the following disclaimer in the
+ *       documentation and/or other materials provided with the distribution.
+ *     * Neither the name of Ajax.org B.V. nor the
+ *       names of its contributors may be used to endorse or promote products
+ *       derived from this software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
+ * ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
+ * WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+ * DISCLAIMED. IN NO EVENT SHALL AJAX.ORG B.V. BE LIABLE FOR ANY
+ * DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
+ * (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
+ * LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
+ * ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+ * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+ * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ *
+ * ***** END LICENSE BLOCK ***** */
+
+define(function(require, exports, module) {
+"use strict";
+
+var oop = require("../lib/oop");
+var DocCommentHighlightRules = require("./doc_comment_highlight_rules").DocCommentHighlightRules;
+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("|")
+    );
+
+    var storageType = (
+        ["Prop", "Type", "Type'", "Type₊", "Type₁", "Type₂", "Type₃"].join("|")
+    );
+
+    var storageModifiers = (
+        "\\[(" +
+            ["persistent", "notation", "parsing-only", "visible", "instance", "class", "prefix", "axioms", "fields",
+             "multiple-instances", "classes", "instances", "coercions", "options", "trust",
+             "coercion", "reducible", "irreducible", "raw"].join("|") +
+            ")\\]"
+    );
+
+    var keywordOperators = (
+        [].join("|")
+    );
+
+    var builtinConstants = (
+        "NULL|true|false|TRUE|FALSE"
+    );
+
+    var keywordMapper = this.$keywords = this.createKeywordMapper({
+        "keyword.control" : keywordControls,
+        "storage.type" : storageType,
+        "keyword.operator" : keywordOperators,
+        "variable.language": "sorry",
+        "constant.language": builtinConstants
+    }, "identifier");
+
+    var identifierRe = "[A-Za-z_\u03b1-\u03ba\u03bc-\u03fb\u1f00-\u1ffe\u2100-\u214f][A-Za-z0-9_'\u03b1-\u03ba\u03bc-\u03fb\u1f00-\u1ffe\u2070-\u2079\u207f-\u2089\u2090-\u209c\u2100-\u214f]*";
+    var operatorRe = new RegExp(["#", "@", "->", "∼", "↔", "/", "==", "=", ":=", "<->",
+                                 "/\\", "\\/", "∧", "∨", "≠", "<", ">", "≤", "≥", "¬",
+                                 "<=", ">=", "⁻¹", "⬝", "▸", "\\+", "\\*", "-", "/",
+                                 "λ", "→", "∃", "∀", ":="].join("|"));
+    // regexp must not have capturing parentheses. Use (?:) instead.
+    // regexps are ordered -> the first match is used
+
+    this.$rules = {
+        "start" : [
+            {
+                token : "comment", // single line comment "--"
+                regex : "--.*$"
+            },
+            DocCommentHighlightRules.getStartRule("doc-start"),
+            {
+                token : "comment", // multi line comment "/-"
+                regex : "\\/-",
+                next : "comment"
+            }, {
+                token : "string", // single line
+                regex : '["](?:(?:\\\\.)|(?:[^"\\\\]))*?["]'
+            }, {
+                token : "string", // multi line string start
+                regex : '["].*\\\\$',
+                next : "qqstring"
+            }, {
+                token : "string", // single line
+                regex : "['](?:(?:\\\\.)|(?:[^'\\\\]))*?[']"
+            }, {
+                token : "string", // multi line string start
+                regex : "['].*\\\\$",
+                next : "qstring"
+            }, {
+                token : "constant.numeric", // hex
+                regex : "0[xX][0-9a-fA-F]+(L|l|UL|ul|u|U|F|f|ll|LL|ull|ULL)?\\b"
+            }, {
+                token : "constant.numeric", // float
+                regex : "[+-]?\\d+(?:(?:\\.\\d*)?(?:[eE][+-]?\\d+)?)?(L|l|UL|ul|u|U|F|f|ll|LL|ull|ULL)?\\b"
+            }, {
+                token : "storage.modifier",
+                regex : storageModifiers
+            }, {
+                token : "keyword", // pre-compiler directives
+                regex : "#\\s*(?:include|import|pragma|line|define|undef|if|ifdef|else|elif|ifndef)\\b",
+                next  : "directive"
+            }, {
+                token : "keyword", // special case pre-compiler directive
+                regex : "(?:#\\s*endif)\\b"
+            }, {
+                token : keywordMapper,
+                regex : identifierRe
+            }, {
+                token : "operator",
+                regex : operatorRe
+            }, {
+              token : "punctuation.operator",
+              regex : "\\?|\\:|\\,|\\;|\\."
+            }, {
+                token : "paren.lparen",
+                regex : "[[({]"
+            }, {
+                token : "paren.rparen",
+                regex : "[\\])}]"
+            }, {
+                token : "text",
+                regex : "\\s+"
+            }
+        ],
+        "comment" : [
+            {
+                token : "comment", // closing comment
+                regex : ".*?-\\/",
+                next : "start"
+            }, {
+                token : "comment", // comment spanning whole line
+                regex : ".+"
+            }
+        ],
+        "qqstring" : [
+            {
+                token : "string",
+                regex : '(?:(?:\\\\.)|(?:[^"\\\\]))*?"',
+                next : "start"
+            }, {
+                token : "string",
+                regex : '.+'
+            }
+        ],
+        "qstring" : [
+            {
+                token : "string",
+                regex : "(?:(?:\\\\.)|(?:[^'\\\\]))*?'",
+                next : "start"
+            }, {
+                token : "string",
+                regex : '.+'
+            }
+        ],
+        "directive" : [
+            {
+                token : "constant.other.multiline",
+                regex : /\\/
+            },
+            {
+                token : "constant.other.multiline",
+                regex : /.*\\/
+            },
+            {
+                token : "constant.other",
+                regex : "\\s*<.+?>",
+                next : "start"
+            },
+            {
+                token : "constant.other", // single line
+                regex : '\\s*["](?:(?:\\\\.)|(?:[^"\\\\]))*?["]',
+                next : "start"
+            },
+            {
+                token : "constant.other", // single line
+                regex : "\\s*['](?:(?:\\\\.)|(?:[^'\\\\]))*?[']",
+                next : "start"
+            },
+            // "\" implies multiline, while "/" implies comment
+            {
+                token : "constant.other",
+                regex : /[^\\\/]+/,
+                next : "start"
+            }
+        ]
+    };
+
+    this.embedRules(DocCommentHighlightRules, "doc-",
+        [ DocCommentHighlightRules.getEndRule("start") ]);
+};
+
+oop.inherits(leanHighlightRules, TextHighlightRules);
+
+exports.leanHighlightRules = leanHighlightRules;
+});
diff --git a/lib/ace/snippets/lean.js b/lib/ace/snippets/lean.js
new file mode 100644
index 00000000..a3c01639
--- /dev/null
+++ b/lib/ace/snippets/lean.js
@@ -0,0 +1,7 @@
+define(function(require, exports, module) {
+"use strict";
+
+exports.snippetText = require("../requirejs/text!./lean.snippets");
+exports.scope = "lean";
+
+});
diff --git a/lib/ace/snippets/lean.snippets b/lib/ace/snippets/lean.snippets
new file mode 100644
index 00000000..e69de29b

From 9654382294dce7bdde7fcbe70e6f2f2613662d3a Mon Sep 17 00:00:00 2001
From: Soonho Kong <soonhok@cs.cmu.edu>
Date: Tue, 24 Feb 2015 11:02:06 -0500
Subject: [PATCH 2/9] use 'defaultToken' for comment/qqstring/qstring in
 lean-mode

Suggested by @nightwing
---
 lib/ace/mode/lean_highlight_rules.js | 36 +++++-----------------------
 1 file changed, 6 insertions(+), 30 deletions(-)

diff --git a/lib/ace/mode/lean_highlight_rules.js b/lib/ace/mode/lean_highlight_rules.js
index d5f9a67c..44eb8d50 100644
--- a/lib/ace/mode/lean_highlight_rules.js
+++ b/lib/ace/mode/lean_highlight_rules.js
@@ -151,36 +151,12 @@ var leanHighlightRules = function() {
                 regex : "\\s+"
             }
         ],
-        "comment" : [
-            {
-                token : "comment", // closing comment
-                regex : ".*?-\\/",
-                next : "start"
-            }, {
-                token : "comment", // comment spanning whole line
-                regex : ".+"
-            }
-        ],
-        "qqstring" : [
-            {
-                token : "string",
-                regex : '(?:(?:\\\\.)|(?:[^"\\\\]))*?"',
-                next : "start"
-            }, {
-                token : "string",
-                regex : '.+'
-            }
-        ],
-        "qstring" : [
-            {
-                token : "string",
-                regex : "(?:(?:\\\\.)|(?:[^'\\\\]))*?'",
-                next : "start"
-            }, {
-                token : "string",
-                regex : '.+'
-            }
-        ],
+        "comment" : [ {token: "comment", regex: "-/", next: "start"},
+                      {defaultToken: "comment"} ],
+        "qqstring" : [ {token : "string", regex : '(?:(?:\\\\.)|(?:[^"\\\\]))*?"', next : "start" },
+                       {defaultToken: "qqstring"} ],
+        "qstring" : [ {token : "string", regex : "(?:(?:\\\\.)|(?:[^'\\\\]))*?'", next : "start" },
+                      {defaultToken: "qstring"} ],
         "directive" : [
             {
                 token : "constant.other.multiline",

From 8f49d3d89784095089bf0885268b4e87e2fbc69c Mon Sep 17 00:00:00 2001
From: Soonho Kong <soonhok@cs.cmu.edu>
Date: Tue, 24 Feb 2015 11:03:02 -0500
Subject: [PATCH 3/9] add a small demo for lean mode

---
 demo/kitchen-sink/docs/lean.lean | 9 +++++++++
 1 file changed, 9 insertions(+)
 create mode 100644 demo/kitchen-sink/docs/lean.lean

diff --git a/demo/kitchen-sink/docs/lean.lean b/demo/kitchen-sink/docs/lean.lean
new file mode 100644
index 00000000..40e82753
--- /dev/null
+++ b/demo/kitchen-sink/docs/lean.lean
@@ -0,0 +1,9 @@
+import logic
+section
+  variables (A : Type) (p q : A → Prop)
+
+  example : (∀x : A, p x ∧ q x) → ∀y : A, p y  :=
+  assume H : ∀x : A, p x ∧ q x,
+  take y : A,
+  show p y, from and.elim_left (H y)
+end

From 74800e84ee204d1fd89a82bab1d71c8d8703e1c4 Mon Sep 17 00:00:00 2001
From: Soonho Kong <soonhok@cs.cmu.edu>
Date: Tue, 24 Feb 2015 12:09:11 -0500
Subject: [PATCH 4/9] remove single quoted string (qstring) from lean-mode

---
 lib/ace/mode/lean_highlight_rules.js | 9 ---------
 1 file changed, 9 deletions(-)

diff --git a/lib/ace/mode/lean_highlight_rules.js b/lib/ace/mode/lean_highlight_rules.js
index 44eb8d50..48241c0e 100644
--- a/lib/ace/mode/lean_highlight_rules.js
+++ b/lib/ace/mode/lean_highlight_rules.js
@@ -108,13 +108,6 @@ var leanHighlightRules = function() {
                 token : "string", // multi line string start
                 regex : '["].*\\\\$',
                 next : "qqstring"
-            }, {
-                token : "string", // single line
-                regex : "['](?:(?:\\\\.)|(?:[^'\\\\]))*?[']"
-            }, {
-                token : "string", // multi line string start
-                regex : "['].*\\\\$",
-                next : "qstring"
             }, {
                 token : "constant.numeric", // hex
                 regex : "0[xX][0-9a-fA-F]+(L|l|UL|ul|u|U|F|f|ll|LL|ull|ULL)?\\b"
@@ -155,8 +148,6 @@ var leanHighlightRules = function() {
                       {defaultToken: "comment"} ],
         "qqstring" : [ {token : "string", regex : '(?:(?:\\\\.)|(?:[^"\\\\]))*?"', next : "start" },
                        {defaultToken: "qqstring"} ],
-        "qstring" : [ {token : "string", regex : "(?:(?:\\\\.)|(?:[^'\\\\]))*?'", next : "start" },
-                      {defaultToken: "qstring"} ],
         "directive" : [
             {
                 token : "constant.other.multiline",

From a0fe09f3bee4197231b18215ab8af02f32146755 Mon Sep 17 00:00:00 2001
From: Soonho Kong <soonhok@cs.cmu.edu>
Date: Tue, 24 Feb 2015 13:19:56 -0500
Subject: [PATCH 5/9] clean up unused rules for lean-mode

---
 lib/ace/mode/lean_highlight_rules.js | 47 +---------------------------
 1 file changed, 1 insertion(+), 46 deletions(-)

diff --git a/lib/ace/mode/lean_highlight_rules.js b/lib/ace/mode/lean_highlight_rules.js
index 48241c0e..f653096b 100644
--- a/lib/ace/mode/lean_highlight_rules.js
+++ b/lib/ace/mode/lean_highlight_rules.js
@@ -70,16 +70,11 @@ var leanHighlightRules = function() {
         [].join("|")
     );
 
-    var builtinConstants = (
-        "NULL|true|false|TRUE|FALSE"
-    );
-
     var keywordMapper = this.$keywords = this.createKeywordMapper({
         "keyword.control" : keywordControls,
         "storage.type" : storageType,
         "keyword.operator" : keywordOperators,
         "variable.language": "sorry",
-        "constant.language": builtinConstants
     }, "identifier");
 
     var identifierRe = "[A-Za-z_\u03b1-\u03ba\u03bc-\u03fb\u1f00-\u1ffe\u2100-\u214f][A-Za-z0-9_'\u03b1-\u03ba\u03bc-\u03fb\u1f00-\u1ffe\u2070-\u2079\u207f-\u2089\u2090-\u209c\u2100-\u214f]*";
@@ -117,13 +112,6 @@ var leanHighlightRules = function() {
             }, {
                 token : "storage.modifier",
                 regex : storageModifiers
-            }, {
-                token : "keyword", // pre-compiler directives
-                regex : "#\\s*(?:include|import|pragma|line|define|undef|if|ifdef|else|elif|ifndef)\\b",
-                next  : "directive"
-            }, {
-                token : "keyword", // special case pre-compiler directive
-                regex : "(?:#\\s*endif)\\b"
             }, {
                 token : keywordMapper,
                 regex : identifierRe
@@ -145,40 +133,7 @@ var leanHighlightRules = function() {
             }
         ],
         "comment" : [ {token: "comment", regex: "-/", next: "start"},
-                      {defaultToken: "comment"} ],
-        "qqstring" : [ {token : "string", regex : '(?:(?:\\\\.)|(?:[^"\\\\]))*?"', next : "start" },
-                       {defaultToken: "qqstring"} ],
-        "directive" : [
-            {
-                token : "constant.other.multiline",
-                regex : /\\/
-            },
-            {
-                token : "constant.other.multiline",
-                regex : /.*\\/
-            },
-            {
-                token : "constant.other",
-                regex : "\\s*<.+?>",
-                next : "start"
-            },
-            {
-                token : "constant.other", // single line
-                regex : '\\s*["](?:(?:\\\\.)|(?:[^"\\\\]))*?["]',
-                next : "start"
-            },
-            {
-                token : "constant.other", // single line
-                regex : "\\s*['](?:(?:\\\\.)|(?:[^'\\\\]))*?[']",
-                next : "start"
-            },
-            // "\" implies multiline, while "/" implies comment
-            {
-                token : "constant.other",
-                regex : /[^\\\/]+/,
-                next : "start"
-            }
-        ]
+                      {defaultToken: "comment"} ]
     };
 
     this.embedRules(DocCommentHighlightRules, "doc-",

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 6/9] 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("|") +
             ")\\]"
     );
 

From 34d80e81cafe90ea78bdb5fcc05fad8a0076bbba Mon Sep 17 00:00:00 2001
From: Soonho Kong <soonhok@cs.cmu.edu>
Date: Tue, 24 Feb 2015 13:21:22 -0500
Subject: [PATCH 7/9] clean up string rule for lean-mode

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

diff --git a/lib/ace/mode/lean_highlight_rules.js b/lib/ace/mode/lean_highlight_rules.js
index 91440169..4ba9d484 100644
--- a/lib/ace/mode/lean_highlight_rules.js
+++ b/lib/ace/mode/lean_highlight_rules.js
@@ -100,12 +100,15 @@ var leanHighlightRules = function() {
                 regex : "\\/-",
                 next : "comment"
             }, {
-                token : "string", // single line
-                regex : '["](?:(?:\\\\.)|(?:[^"\\\\]))*?["]'
+                stateName: "qqstring",
+                token : "string.start", regex : '"', next : [
+                    {token : "string.end", regex : '"', next : "start"},
+                    {token : "string", regex : "\\\\$", next  : "qqstring"},
+                    {token : "string", regex : "\\n$", next  : "qqstring"},
+                    {token : "constant.language.escape", regex : /\\./},
+                    {defaultToken: "string"}
+                ]
             }, {
-                token : "string", // multi line string start
-                regex : '["].*\\\\$',
-                next : "qqstring"
             }, {
                 token : "constant.numeric", // hex
                 regex : "0[xX][0-9a-fA-F]+(L|l|UL|ul|u|U|F|f|ll|LL|ull|ULL)?\\b"
@@ -141,6 +144,7 @@ var leanHighlightRules = function() {
 
     this.embedRules(DocCommentHighlightRules, "doc-",
         [ DocCommentHighlightRules.getEndRule("start") ]);
+    this.normalizeRules();
 };
 
 oop.inherits(leanHighlightRules, TextHighlightRules);

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 8/9] 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"

From 49ff50463939d1a5577088dfeab80bdb91614602 Mon Sep 17 00:00:00 2001
From: Soonho Kong <soonhok@cs.cmu.edu>
Date: Tue, 24 Feb 2015 14:10:41 -0500
Subject: [PATCH 9/9] fix qqstring rule in lean-mode

---
 lib/ace/mode/lean_highlight_rules.js | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/lib/ace/mode/lean_highlight_rules.js b/lib/ace/mode/lean_highlight_rules.js
index 06669de3..d4a37d20 100644
--- a/lib/ace/mode/lean_highlight_rules.js
+++ b/lib/ace/mode/lean_highlight_rules.js
@@ -106,9 +106,7 @@ var leanHighlightRules = function() {
                 stateName: "qqstring",
                 token : "string.start", regex : '"', next : [
                     {token : "string.end", regex : '"', next : "start"},
-                    {token : "string", regex : "\\\\$", next  : "qqstring"},
-                    {token : "string", regex : "\\n$", next  : "qqstring"},
-                    {token : "constant.language.escape", regex : /\\./},
+                    {token : "constant.language.escape", regex : /\\[n"\\]/},
                     {defaultToken: "string"}
                 ]
             }, {