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