clarified signature: prefer enum types;
authorwenzelm
Tue, 29 Aug 2023 19:20:51 +0200
changeset 78616 9acd819db33a
parent 78615 abdf38ee314a
child 78617 2c3a05b297f4
clarified signature: prefer enum types;
src/Tools/Graphview/model.scala
src/Tools/Graphview/mutator_dialog.scala
src/Tools/Graphview/mutator_event.scala
--- a/src/Tools/Graphview/model.scala	Tue Aug 29 19:17:25 2023 +0200
+++ b/src/Tools/Graphview/model.scala	Tue Aug 29 19:20:51 2023 +0200
@@ -20,12 +20,12 @@
   def apply(): List[Mutator.Info] = _mutators
   def apply(mutators: List[Mutator.Info]): Unit = {
     _mutators = mutators
-    events.event(Mutator_Event.New_List(mutators))
+    events.event(Mutator_Event.Message.New_List(mutators))
   }
 
   def add(mutator: Mutator.Info): Unit = {
     _mutators = _mutators ::: List(mutator)
-    events.event(Mutator_Event.Add(mutator))
+    events.event(Mutator_Event.Message.Add(mutator))
   }
 }
 
--- a/src/Tools/Graphview/mutator_dialog.scala	Tue Aug 29 19:17:25 2023 +0200
+++ b/src/Tools/Graphview/mutator_dialog.scala	Tue Aug 29 19:20:51 2023 +0200
@@ -37,8 +37,8 @@
 
   container.events +=
     {
-      case Mutator_Event.Add(m) => add_panel(new Mutator_Panel(m))
-      case Mutator_Event.New_List(ms) => panels = get_panels(ms)
+      case Mutator_Event.Message.Add(m) => add_panel(new Mutator_Panel(m))
+      case Mutator_Event.Message.New_List(ms) => panels = get_panels(ms)
     }
 
   override def open(): Unit = {
--- a/src/Tools/Graphview/mutator_event.scala	Tue Aug 29 19:17:25 2023 +0200
+++ b/src/Tools/Graphview/mutator_event.scala	Tue Aug 29 19:20:51 2023 +0200
@@ -12,9 +12,10 @@
 
 
 object Mutator_Event {
-  sealed abstract class Message
-  case class Add(m: Mutator.Info) extends Message
-  case class New_List(m: List[Mutator.Info]) extends Message
+  enum Message {
+    case Add(m: Mutator.Info) extends Message
+    case New_List(m: List[Mutator.Info]) extends Message
+  }
 
   type Receiver = Message => Unit