tuned;

--- a/src/Tools/jEdit/src/tree_text_area.scala	Sat Nov 02 16:03:26 2024 +0100
+++ b/src/Tools/jEdit/src/tree_text_area.scala	Sat Nov 02 16:08:26 2024 +0100
@@ -87,13 +87,13 @@
 
   def handle_focus(): Unit = ()
 
-  def init_gui(component: JComponent): Unit = {
-    component.addComponentListener(
+  def init_gui(parent: JComponent): Unit = {
+    parent.addComponentListener(
       new ComponentAdapter {
         override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke()
         override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
       })
-    component.addFocusListener(
+    parent.addFocusListener(
       new FocusAdapter {
         override def focusGained(e: FocusEvent): Unit = handle_focus()
       })
@@ -106,7 +106,7 @@
         }
       })
 
-    component match {
+    parent match {
       case dockable: Dockable => dockable.set_content(main_pane)
       case _ =>
     }