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-",