--- a/src/Tools/jEdit/src/query_dockable.scala Thu May 08 00:14:06 2014 +0200
+++ b/src/Tools/jEdit/src/query_dockable.scala Thu May 08 11:47:38 2014 +0200
@@ -123,7 +123,7 @@
private val control_panel =
new Wrap_Panel(Wrap_Panel.Alignment.Right)(
query_label, Component.wrap(query), limit, allow_dups,
- process_indicator.component, apply_button, pretty_text_area.detach_button,
+ process_indicator.component, apply_button,
pretty_text_area.search_label, pretty_text_area.search_pattern)
def select { control_panel.contents += zoom }
@@ -171,8 +171,7 @@
private val control_panel =
new Wrap_Panel(Wrap_Panel.Alignment.Right)(
- query_label, Component.wrap(query), process_indicator.component,
- apply_button, pretty_text_area.detach_button,
+ query_label, Component.wrap(query), process_indicator.component, apply_button,
pretty_text_area.search_label, pretty_text_area.search_pattern)
def select { control_panel.contents += zoom }
@@ -258,7 +257,7 @@
set_selector()
control_panel.contents.clear
control_panel.contents ++=
- List(query_label, selector, apply_button, pretty_text_area.detach_button,
+ List(query_label, selector, apply_button,
pretty_text_area.search_label, pretty_text_area.search_pattern, zoom)
}