# HG changeset patch
# User wenzelm
# Date 1731870897 -3600
# Node ID c9256ac992147653e808445b075afe6aa6996ff7
# Parent  97a32b4d29e51a81a8971fcc5a557b8390c3651a
clarified signature;

diff -r 97a32b4d29e5 -r c9256ac99214 src/Tools/jEdit/src/debugger_dockable.scala
--- 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()
   }
diff -r 97a32b4d29e5 -r c9256ac99214 src/Tools/jEdit/src/output_area.scala
--- 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()
 }
diff -r 97a32b4d29e5 -r c9256ac99214 src/Tools/jEdit/src/output_dockable.scala
--- 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()
   }
 }