--- a/src/Tools/jEdit/src/session_build.scala Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Tools/jEdit/src/session_build.scala Thu Mar 04 21:04:27 2021 +0100
@@ -80,10 +80,10 @@
private def set_actions(cs: Component*): Unit =
{
- action_panel.contents.clear
+ action_panel.contents.clear()
action_panel.contents ++= cs
- layout_panel.revalidate
- layout_panel.repaint
+ layout_panel.revalidate()
+ layout_panel.repaint()
}
@@ -94,7 +94,7 @@
private def return_code(rc: Int): Unit =
GUI_Thread.later {
_return_code = Some(rc)
- delay_exit.invoke
+ delay_exit.invoke()
}
private val delay_exit =
@@ -129,7 +129,7 @@
private def stopping(): Unit =
{
- progress.stop
+ progress.stop()
set_actions(new Label("Stopping ..."))
}