--- 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 */