--- 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)
--- 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)
--- 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)
--- 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 = {
--- 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 =
--- 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)
}
--- 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)