equal
deleted
inserted
replaced
82 tooltip = selection_label.tooltip |
82 tooltip = selection_label.tooltip |
83 } |
83 } |
84 private val selection_field_foreground = selection_field.foreground |
84 private val selection_field_foreground = selection_field.foreground |
85 |
85 |
86 private val selection_delay = |
86 private val selection_delay = |
87 GUI_Thread.delay_last(visualizer.get_options.seconds("editor_input_delay")) { |
87 GUI_Thread.delay_last(visualizer.options.seconds("editor_input_delay")) { |
88 val (pattern, ok) = |
88 val (pattern, ok) = |
89 selection_field.text match { |
89 selection_field.text match { |
90 case null | "" => (None, true) |
90 case null | "" => (None, true) |
91 case s => |
91 case s => |
92 val pattern = Library.make_regex(s) |
92 val pattern = Library.make_regex(s) |