src/Tools/jEdit/src/session_build.scala
changeset 73367 77ef8bef0593
parent 73340 0ffcad1f6130
child 74068 62e4ec8cff38
--- 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 ..."))
     }