--- a/src/Pure/library.scala Wed Jan 11 14:22:57 2017 +0100
+++ b/src/Pure/library.scala Wed Jan 11 14:48:07 2017 +0100
@@ -196,6 +196,15 @@
def make_regex(s: String): Option[Regex] =
try { Some(new Regex(s)) } catch { case ERROR(_) => None }
+ def is_regex_meta(c: Char): Boolean = """()[]{}\^$|?*+.<>-=!""".contains(c)
+
+ def escape_regex(s: String): String =
+ if (s.exists(is_regex_meta(_))) {
+ (for (c <- s.iterator)
+ yield { if (is_regex_meta(c)) "\\" + c.toString else c.toString }).mkString
+ }
+ else s
+
/* lists */
--- a/src/Tools/VSCode/src/grammar.scala Wed Jan 11 14:22:57 2017 +0100
+++ b/src/Tools/VSCode/src/grammar.scala Wed Jan 11 14:48:07 2017 +0100
@@ -40,11 +40,8 @@
val keywords3 = major_keywords(Set(Keyword.PRF_ASM, Keyword.PRF_ASM_GOAL))
- def quote_name(a: String): String =
- if (Symbol.is_ascii_identifier(a)) a else "\\Q" + a + "\\E"
-
def grouped_names(as: List[String]): String =
- JSON.Format("\\b(" + as.sorted.map(quote_name(_)).mkString("|") + ")\\b")
+ JSON.Format("\\b(" + as.sorted.map(Library.escape_regex(_)).mkString("|") + ")\\b")
"""{
"name": "Isabelle",