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