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