# HG changeset patch
# User wenzelm
# Date 1484142487 -3600
# Node ID 2d594dabcca653e70e301b8ec9adde11848613b5
# Parent  41e2797af4963b09327b8acdb30130c6f4182695
tuned;

diff -r 41e2797af496 -r 2d594dabcca6 src/Pure/library.scala
--- 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 */
 
diff -r 41e2797af496 -r 2d594dabcca6 src/Tools/VSCode/src/grammar.scala
--- 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",