# HG changeset patch
# User wenzelm
# Date 1730559598 -3600
# Node ID fad1278d0f5b8ece2e1bab53a9b5959fe8f44413
# Parent  5f28bded8d7d75921b34a0b27af6a339ffddd9b3
clarified signature;

diff -r 5f28bded8d7d -r fad1278d0f5b src/Tools/jEdit/src/debugger_dockable.scala
--- a/src/Tools/jEdit/src/debugger_dockable.scala	Sat Nov 02 15:42:37 2024 +0100
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Sat Nov 02 15:59:58 2024 +0100
@@ -102,9 +102,7 @@
   override def detach_operation: Option[() => Unit] =
     tree_text_area.pretty_text_area.detach_operation
 
-  set_content(tree_text_area.main_pane)
-  addComponentListener(tree_text_area.component_resize)
-  addFocusListener(tree_text_area.component_focus)
+  tree_text_area.init_gui(dockable)
 
 
   /* tree view */
diff -r 5f28bded8d7d -r fad1278d0f5b src/Tools/jEdit/src/tree_text_area.scala
--- a/src/Tools/jEdit/src/tree_text_area.scala	Sat Nov 02 15:42:37 2024 +0100
+++ b/src/Tools/jEdit/src/tree_text_area.scala	Sat Nov 02 15:59:58 2024 +0100
@@ -12,7 +12,7 @@
 import java.awt.{BorderLayout, Dimension}
 import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent, FocusAdapter, FocusEvent,
   MouseEvent, MouseAdapter}
-import javax.swing.{JTree, JMenuItem}
+import javax.swing.{JTree, JMenuItem, JComponent}
 import javax.swing.tree.{DefaultMutableTreeNode, DefaultTreeModel, TreeSelectionModel}
 import javax.swing.event.{TreeSelectionEvent, TreeSelectionListener}
 
@@ -68,20 +68,9 @@
   lazy val delay_resize: Delay =
     Delay.first(PIDE.session.update_delay, gui = true) { handle_resize() }
 
-  lazy val component_resize: ComponentAdapter =
-    new ComponentAdapter {
-      override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke()
-      override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
-    }
-
 
   /* main pane */
 
-  def handle_focus(): Unit = ()
-
-  lazy val component_focus: FocusAdapter =
-    new FocusAdapter { override def focusGained(e: FocusEvent): Unit = handle_focus() }
-
   val tree_pane: ScrollPane = new ScrollPane(Component.wrap(tree))
   tree_pane.horizontalScrollBarPolicy = ScrollPane.BarPolicy.Always
   tree_pane.verticalScrollBarPolicy = ScrollPane.BarPolicy.Always
@@ -92,4 +81,26 @@
     leftComponent = tree_pane
     rightComponent = Component.wrap(pretty_text_area)
   }
+
+
+  /* GUI component */
+
+  def handle_focus(): Unit = ()
+
+  def init_gui(component: JComponent): Unit = {
+    component.addComponentListener(
+      new ComponentAdapter {
+        override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke()
+        override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
+      })
+    component.addFocusListener(
+      new FocusAdapter {
+        override def focusGained(e: FocusEvent): Unit = handle_focus()
+      })
+
+    component match {
+      case dockable: Dockable => dockable.set_content(main_pane)
+      case _ =>
+    }
+  }
 }