# HG changeset patch
# User wenzelm
# Date 1730558143 -3600
# Node ID a00d4d50b8513d9806ba67b5f2a43525505b72c5
# Parent  ea3cae90f76b2e15046c35fe130cbbb2653f7264
clarified signature;

diff -r ea3cae90f76b -r a00d4d50b851 src/Tools/jEdit/src/debugger_dockable.scala
--- a/src/Tools/jEdit/src/debugger_dockable.scala	Sat Nov 02 15:28:17 2024 +0100
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Sat Nov 02 15:35:43 2024 +0100
@@ -101,6 +101,7 @@
     tree_text_area.pretty_text_area.detach_operation
 
   set_content(tree_text_area.main_pane)
+  addComponentListener(tree_text_area.component_resize)
 
 
   /* tree view */
@@ -310,19 +311,8 @@
   override def exit(): Unit = {
     PIDE.session.global_options -= main
     PIDE.session.debugger_updates -= main
-    delay_resize.revoke()
+    tree_text_area.delay_resize.revoke()
     debugger.exit(dockable)
     jEdit.propertiesChanged()
   }
-
-
-  /* resize */
-
-  private val delay_resize =
-    Delay.first(PIDE.session.update_delay, gui = true) { tree_text_area.handle_resize() }
-
-  addComponentListener(new ComponentAdapter {
-    override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke()
-    override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
-  })
 }
diff -r ea3cae90f76b -r a00d4d50b851 src/Tools/jEdit/src/tree_text_area.scala
--- a/src/Tools/jEdit/src/tree_text_area.scala	Sat Nov 02 15:28:17 2024 +0100
+++ b/src/Tools/jEdit/src/tree_text_area.scala	Sat Nov 02 15:35:43 2024 +0100
@@ -65,6 +65,15 @@
   def handle_resize(): Unit = ()
   def handle_update(): Unit = ()
 
+  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 */