src/Tools/Graphview/model.scala
changeset 75393 87ebf5a50283
parent 73359 d8a0e996614b
child 78616 9acd819db33a
--- a/src/Tools/Graphview/model.scala	Fri Apr 01 11:51:42 2022 +0200
+++ b/src/Tools/Graphview/model.scala	Fri Apr 01 17:06:10 2022 +0200
@@ -13,28 +13,24 @@
 import java.awt.Color
 
 
-class Mutator_Container(val available: List[Mutator])
-{
+class Mutator_Container(val available: List[Mutator]) {
   val events = new Mutator_Event.Bus
 
   private var _mutators : List[Mutator.Info] = Nil
   def apply(): List[Mutator.Info] = _mutators
-  def apply(mutators: List[Mutator.Info]): Unit =
-  {
+  def apply(mutators: List[Mutator.Info]): Unit = {
     _mutators = mutators
     events.event(Mutator_Event.New_List(mutators))
   }
 
-  def add(mutator: Mutator.Info): Unit =
-  {
+  def add(mutator: Mutator.Info): Unit = {
     _mutators = _mutators ::: List(mutator)
     events.event(Mutator_Event.Add(mutator))
   }
 }
 
 
-class Model(val full_graph: Graph_Display.Graph)
-{
+class Model(val full_graph: Graph_Display.Graph) {
   val Mutators =
     new Mutator_Container(
       List(
@@ -61,8 +57,7 @@
   private var _colors = Map.empty[Graph_Display.Node, Color]
   def colors = _colors
 
-  private def build_colors(): Unit =
-  {
+  private def build_colors(): Unit = {
     _colors =
       Colors().foldLeft(Map.empty[Graph_Display.Node, Color]) {
         case (colors, m) =>