--- 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