src/Tools/Graphview/mutator_dialog.scala
changeset 73367 77ef8bef0593
parent 73357 31d4274f32de
child 75393 87ebf5a50283
--- a/src/Tools/Graphview/mutator_dialog.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Tools/Graphview/mutator_dialog.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -46,7 +46,7 @@
   override def open(): Unit =
   {
     if (!visible) panels = get_panels(container())
-    super.open
+    super.open()
   }
 
   minimumSize = new Dimension(700, 200)
@@ -94,8 +94,8 @@
 
   def paint_panels(): Unit =
   {
-    Focus_Traveral_Policy.clear
-    filter_panel.contents.clear
+    Focus_Traveral_Policy.clear()
+    filter_panel.contents.clear()
     panels.map(x => {
         filter_panel.contents += x
         Focus_Traveral_Policy.addAll(x.focusList)
@@ -106,8 +106,8 @@
     Focus_Traveral_Policy.add(add_button.peer)
     Focus_Traveral_Policy.add(apply_button.peer)
     Focus_Traveral_Policy.add(cancel_button.peer)
-    filter_panel.revalidate
-    filter_panel.repaint
+    filter_panel.revalidate()
+    filter_panel.repaint()
   }
 
   val filter_panel: BoxPanel = new BoxPanel(Orientation.Vertical) {}
@@ -130,7 +130,7 @@
   }
 
   private val cancel_button = new Button {
-    action = Action("Close") { close }
+    action = Action("Close") { close() }
   }
   defaultButton = cancel_button