# HG changeset patch
# User wenzelm
# Date 1399409744 -7200
# Node ID 87ebb99786ed02c878e560782b3ecc72de268196
# Parent  3020f6bbd1190e9c53b6ea8d1a58756f331157e0
tuned GUI layout;

diff -r 3020f6bbd119 -r 87ebb99786ed src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Tue May 06 22:47:55 2014 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Tue May 06 22:55:44 2014 +0200
@@ -142,7 +142,7 @@
 
   private val controls =
     new Wrap_Panel(Wrap_Panel.Alignment.Right)(
-      pretty_text_area.search_label, pretty_text_area.search_pattern,
-      auto_update, update, pretty_text_area.detach_button, zoom)
+      auto_update, update, pretty_text_area.detach_button,
+      pretty_text_area.search_label, pretty_text_area.search_pattern, zoom)
   add(controls.peer, BorderLayout.NORTH)
 }
diff -r 3020f6bbd119 -r 87ebb99786ed src/Tools/jEdit/src/query_dockable.scala
--- a/src/Tools/jEdit/src/query_dockable.scala	Tue May 06 22:47:55 2014 +0200
+++ b/src/Tools/jEdit/src/query_dockable.scala	Tue May 06 22:55:44 2014 +0200
@@ -123,9 +123,8 @@
     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.search_label, pretty_text_area.search_pattern,
-        pretty_text_area.detach_button)
+        process_indicator.component, apply_button, pretty_text_area.detach_button,
+        pretty_text_area.search_label, pretty_text_area.search_pattern)
 
     def select { control_panel.contents += zoom }
 
@@ -172,9 +171,9 @@
 
     private val control_panel =
       new Wrap_Panel(Wrap_Panel.Alignment.Right)(
-        query_label, Component.wrap(query), process_indicator.component, apply_button,
-        pretty_text_area.search_label, pretty_text_area.search_pattern,
-        pretty_text_area.detach_button)
+        query_label, Component.wrap(query), process_indicator.component,
+        apply_button, pretty_text_area.detach_button,
+        pretty_text_area.search_label, pretty_text_area.search_pattern)
 
     def select { control_panel.contents += zoom }
 
@@ -259,9 +258,8 @@
       set_selector()
       control_panel.contents.clear
       control_panel.contents ++=
-        List(query_label, selector, apply_button,
-          pretty_text_area.search_label, pretty_text_area.search_pattern,
-          pretty_text_area.detach_button, zoom)
+        List(query_label, selector, apply_button, pretty_text_area.detach_button,
+          pretty_text_area.search_label, pretty_text_area.search_pattern, zoom)
     }
 
     val page =