clarified signature;
authorwenzelm
Sat, 02 Nov 2024 15:35:43 +0100
changeset 81312 a00d4d50b851
parent 81311 ea3cae90f76b
child 81313 5f28bded8d7d
clarified signature;
src/Tools/jEdit/src/debugger_dockable.scala
src/Tools/jEdit/src/tree_text_area.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()
-  })
 }
--- 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 */