src/Pure/library.scala

--- a/src/Pure/library.scala	Thu Jan 01 14:05:48 2015 +0100
+++ b/src/Pure/library.scala	Thu Jan 01 14:21:26 2015 +0100
@@ -9,6 +9,7 @@
 
 
 import scala.collection.mutable
+import scala.util.matching.Regex
 
 
 object Library
@@ -186,6 +187,12 @@
   }
 
 
+  /* regular expressions */
+
+  def make_regex(s: String): Option[Regex] =
+    try { Some(new Regex(s)) } catch { case ERROR(_) => None }
+
+
   /* canonical list operations */
 
   def member[A, B](xs: List[A])(x: B): Boolean = xs.exists(_ == x)