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 */