clarified signature;
authorwenzelm
Sun, 17 Nov 2024 20:14:57 +0100
changeset 81477 c9256ac99214
parent 81476 97a32b4d29e5
child 81478 a774655375ed
clarified signature;
src/Tools/jEdit/src/debugger_dockable.scala
src/Tools/jEdit/src/output_area.scala
src/Tools/jEdit/src/output_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()
   }
--- 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()
   }
 }