src/Tools/jEdit/src/state_dockable.scala
changeset 73340 0ffcad1f6130
parent 71704 b9a5eb0f3b43
child 73987 fc363a3b690a
--- a/src/Tools/jEdit/src/state_dockable.scala	Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src/state_dockable.scala	Mon Mar 01 22:22:12 2021 +0100
@@ -43,11 +43,11 @@
     Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }
 
   addComponentListener(new ComponentAdapter {
-    override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
-    override def componentShown(e: ComponentEvent) { delay_resize.invoke() }
+    override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke()
+    override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
   })
 
-  private def handle_resize()
+  private def handle_resize(): Unit =
   {
     GUI_Thread.require {}
 
@@ -61,7 +61,7 @@
   def update_request(): Unit =
     GUI_Thread.require { print_state.apply_query(Nil) }
 
-  def update()
+  def update(): Unit =
   {
     GUI_Thread.require {}
 
@@ -126,7 +126,7 @@
         GUI_Thread.later { auto_update() }
     }
 
-  override def init()
+  override def init(): Unit =
   {
     PIDE.session.global_options += main
     PIDE.session.commands_changed += main
@@ -136,7 +136,7 @@
     auto_update()
   }
 
-  override def exit()
+  override def exit(): Unit =
   {
     print_state.deactivate()
     PIDE.session.caret_focus -= main