# HG changeset patch
# User wenzelm
# Date 1730927045 -3600
# Node ID cbfc76aace10bc580c5ebe947d201c30ced0808c
# Parent  969280db8ca5eafa4d11eeca00ca001afbf148ba
tuned signature;

diff -r 969280db8ca5 -r cbfc76aace10 src/Tools/jEdit/src/debugger_dockable.scala
--- a/src/Tools/jEdit/src/debugger_dockable.scala	Wed Nov 06 16:07:30 2024 +0100
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Wed Nov 06 22:04:05 2024 +0100
@@ -239,9 +239,9 @@
       List(
         break_button, continue_button, step_button, step_over_button, step_out_button,
         context_label, Component.wrap(context_field),
-        expression_label, Component.wrap(expression_field), eval_button, sml_button,
-        output.pretty_text_area.search_label,
-        output.pretty_text_area.search_field, zoom))
+        expression_label, Component.wrap(expression_field), eval_button, sml_button) :::
+      output.pretty_text_area.search_components :::
+      List(output.pretty_text_area.search_field, zoom))
 
   add(controls.peer, BorderLayout.NORTH)
 
diff -r 969280db8ca5 -r cbfc76aace10 src/Tools/jEdit/src/info_dockable.scala
--- a/src/Tools/jEdit/src/info_dockable.scala	Wed Nov 06 16:07:30 2024 +0100
+++ b/src/Tools/jEdit/src/info_dockable.scala	Wed Nov 06 22:04:05 2024 +0100
@@ -88,8 +88,7 @@
     override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
   })
 
-  private val controls =
-    Wrap_Panel(List(pretty_text_area.search_label, pretty_text_area.search_field, zoom))
+  private val controls = Wrap_Panel(pretty_text_area.search_components ::: List(zoom))
 
   add(controls.peer, BorderLayout.NORTH)
 
diff -r 969280db8ca5 -r cbfc76aace10 src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Wed Nov 06 16:07:30 2024 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala	Wed Nov 06 22:04:05 2024 +0100
@@ -82,8 +82,8 @@
 
   private val controls =
     Wrap_Panel(
-      List(output_state_button, auto_hovering_button, auto_update_button,
-        update_button, pretty_text_area.search_label, pretty_text_area.search_field, zoom))
+      List(output_state_button, auto_hovering_button, auto_update_button, update_button) :::
+      pretty_text_area.search_components ::: List(zoom))
 
   add(controls.peer, BorderLayout.NORTH)
 
diff -r 969280db8ca5 -r cbfc76aace10 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Wed Nov 06 16:07:30 2024 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Wed Nov 06 22:04:05 2024 +0100
@@ -170,6 +170,8 @@
       setFont(GUI.imitate_font(getFont, scale = 1.2))
     })
 
+  def search_components: List[Component] = List(search_label, search_field)
+
   private val search_field_foreground = search_field.foreground
 
   private def search_action(text_field: JTextField): Unit = {
diff -r 969280db8ca5 -r cbfc76aace10 src/Tools/jEdit/src/query_dockable.scala
--- a/src/Tools/jEdit/src/query_dockable.scala	Wed Nov 06 16:07:30 2024 +0100
+++ b/src/Tools/jEdit/src/query_dockable.scala	Wed Nov 06 22:04:05 2024 +0100
@@ -118,8 +118,8 @@
     private val control_panel =
       Wrap_Panel(
         List(query_label, Component.wrap(query), limit, allow_dups,
-          process_indicator.component, apply_button,
-          pretty_text_area.search_label, pretty_text_area.search_field))
+          process_indicator.component, apply_button) :::
+        pretty_text_area.search_components)
 
     def select(): Unit = { control_panel.contents += zoom }
 
@@ -166,9 +166,8 @@
 
     private val control_panel =
       Wrap_Panel(
-        List(
-          query_label, Component.wrap(query), process_indicator.component, apply_button,
-          pretty_text_area.search_label, pretty_text_area.search_field))
+        List(query_label, Component.wrap(query), process_indicator.component, apply_button) :::
+        pretty_text_area.search_components)
 
     def select(): Unit = { control_panel.contents += zoom }
 
@@ -252,8 +251,8 @@
       control_panel.contents += query_label
       update_items().foreach(item => control_panel.contents += item.gui)
       control_panel.contents ++=
-        List(process_indicator.component, apply_button,
-          pretty_text_area.search_label, pretty_text_area.search_field, zoom)
+        List(process_indicator.component, apply_button) :::
+        pretty_text_area.search_components ::: List(zoom)
     }
 
     val page =
diff -r 969280db8ca5 -r cbfc76aace10 src/Tools/jEdit/src/simplifier_trace_window.scala
--- a/src/Tools/jEdit/src/simplifier_trace_window.scala	Wed Nov 06 16:07:30 2024 +0100
+++ b/src/Tools/jEdit/src/simplifier_trace_window.scala	Wed Nov 06 22:04:05 2024 +0100
@@ -177,8 +177,7 @@
 
   /* controls */
 
-  private val controls =
-    Wrap_Panel(List(pretty_text_area.search_label, pretty_text_area.search_field, zoom))
+  private val controls = Wrap_Panel(pretty_text_area.search_components ::: List(zoom))
 
   peer.add(controls.peer, BorderLayout.NORTH)
 }
diff -r 969280db8ca5 -r cbfc76aace10 src/Tools/jEdit/src/state_dockable.scala
--- a/src/Tools/jEdit/src/state_dockable.scala	Wed Nov 06 16:07:30 2024 +0100
+++ b/src/Tools/jEdit/src/state_dockable.scala	Wed Nov 06 22:04:05 2024 +0100
@@ -97,8 +97,8 @@
 
   private val controls =
     Wrap_Panel(
-      List(auto_update_button, update_button,
-        locate_button, pretty_text_area.search_label, pretty_text_area.search_field, zoom))
+      List(auto_update_button, update_button, locate_button) :::
+      pretty_text_area.search_components ::: List(zoom))
 
   add(controls.peer, BorderLayout.NORTH)