# HG changeset patch
# User wenzelm
# Date 1730560106 -3600
# Node ID 6a4d718365494f1de1f25075a982201197a1f19e
# Parent  b796e59ec3efb8373173bb03d1ed249dc75ec926
tuned;

diff -r b796e59ec3ef -r 6a4d71836549 src/Tools/jEdit/src/tree_text_area.scala
--- 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 _ =>
     }