# HG changeset patch
# User wenzelm
# Date 1420118486 -3600
# Node ID e3f90d5c00060d0f8cb9f679f5daf1d96a1198de
# Parent  d1e233b4125b97da5065c3ff0307f31dd8fc9efe
tuned;

diff -r d1e233b4125b -r e3f90d5c0006 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)
diff -r d1e233b4125b -r e3f90d5c0006 src/Tools/Graphview/mutator_dialog.scala
--- a/src/Tools/Graphview/mutator_dialog.scala	Thu Jan 01 14:05:48 2015 +0100
+++ b/src/Tools/Graphview/mutator_dialog.scala	Thu Jan 01 14:21:26 2015 +0100
@@ -243,27 +243,16 @@
 
     focusList = focusList.reverse
 
-    private def isRegex(regex: String): Boolean =
-    {
-      try { regex.r; true }
-      catch { case _: java.util.regex.PatternSyntaxException =>  false }
-    }
-
     def get_mutator: Mutator.Info =
     {
-      def regexOrElse(regex: String, orElse: String): String =
-      {
-        if (isRegex(regex)) regex
-        else orElse
-      }
-
       val m =
         initials.mutator match {
           case Mutator.Identity() =>
             Mutator.Identity()
           case Mutator.Node_Expression(r, _, _, _) =>
+            val r1 = inputs(2)._2.get_string
             Mutator.Node_Expression(
-              regexOrElse(inputs(2)._2.get_string, r),
+              if (Library.make_regex(r1).isDefined) r1 else r,
               inputs(3)._2.get_bool,
               // "Parents" means "Show parents" or "Matching Children"
               inputs(1)._2.get_bool,
@@ -280,7 +269,8 @@
               inputs(0)._2.get_string,
               inputs(1)._2.get_string)
           case Mutator.Add_Node_Expression(r) =>
-            Mutator.Add_Node_Expression(regexOrElse(inputs(0)._2.get_string, r))
+            val r1 = inputs(0)._2.get_string
+            Mutator.Add_Node_Expression(if (Library.make_regex(r1).isDefined) r1 else r)
           case Mutator.Add_Transitive_Closure(_, _) =>
             Mutator.Add_Transitive_Closure(
               inputs(0)._2.get_bool,
@@ -298,7 +288,7 @@
           List(
             ("", new iCheckBox("Parents", check_children)),
             ("", new iCheckBox("Children", check_parents)),
-            ("Regex", new iTextField(regex, x => !isRegex(x))),
+            ("Regex", new iTextField(regex, x => Library.make_regex(x).isEmpty)),
             ("", new iCheckBox(reverse_caption, reverse)))
         case Mutator.Node_List(list, reverse, check_parents, check_children) =>
           List(
@@ -311,7 +301,7 @@
             ("Source", new iTextField(source)),
             ("Destination", new iTextField(dest)))
         case Mutator.Add_Node_Expression(regex) =>
-          List(("Regex", new iTextField(regex, x => !isRegex(x))))
+          List(("Regex", new iTextField(regex, x => Library.make_regex(x).isEmpty)))
         case Mutator.Add_Transitive_Closure(parents, children) =>
           List(
             ("", new iCheckBox("Parents", parents)),
diff -r d1e233b4125b -r e3f90d5c0006 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Thu Jan 01 14:05:48 2015 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Thu Jan 01 14:21:26 2015 +0100
@@ -212,8 +212,8 @@
       text_field.getText match {
         case null | "" => (None, true)
         case s =>
-          try { (Some(new Regex(s)), true) }
-          catch { case ERROR(_) => (None, false) }
+          val re = Library.make_regex(s)
+          (re, re.isDefined)
       }
     if (current_search_pattern != pattern) {
       current_search_pattern = pattern