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