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