--- a/src/Tools/jEdit/src/debugger_dockable.scala Sun Nov 17 19:59:10 2024 +0100
+++ b/src/Tools/jEdit/src/debugger_dockable.scala Sun Nov 17 20:14:57 2024 +0100
@@ -279,14 +279,14 @@
PIDE.session.global_options += main
PIDE.session.debugger_updates += main
debugger.init(dockable)
- output.handle_update()
+ output.init()
jEdit.propertiesChanged()
}
override def exit(): Unit = {
PIDE.session.global_options -= main
PIDE.session.debugger_updates -= main
- output.delay_resize.revoke()
+ output.exit()
debugger.exit(dockable)
jEdit.propertiesChanged()
}
--- a/src/Tools/jEdit/src/output_area.scala Sun Nov 17 19:59:10 2024 +0100
+++ b/src/Tools/jEdit/src/output_area.scala Sun Nov 17 20:14:57 2024 +0100
@@ -133,4 +133,8 @@
case _ =>
}
}
+
+ def init(): Unit = handle_update()
+
+ def exit(): Unit = delay_resize.revoke()
}
--- a/src/Tools/jEdit/src/output_dockable.scala Sun Nov 17 19:59:10 2024 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala Sun Nov 17 20:14:57 2024 +0100
@@ -114,13 +114,13 @@
PIDE.session.global_options += main
PIDE.session.commands_changed += main
PIDE.session.caret_focus += main
- handle_update(true)
+ output.init()
}
override def exit(): Unit = {
PIDE.session.global_options -= main
PIDE.session.commands_changed -= main
PIDE.session.caret_focus -= main
- output.delay_resize.revoke()
+ output.exit()
}
}