src/Tools/jEdit/src/pretty_text_area.scala
changeset 59224 e3f90d5c0006
parent 59077 7e0d3da6e6d8
child 59286 ac74eedb910a
--- 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