# HG changeset patch # User wenzelm # Date 1693329651 -7200 # Node ID 9acd819db33ac258a891eaf01fdf8789c60bf3dc # Parent abdf38ee314ad58c45095d02624d11350edee072 clarified signature: prefer enum types; diff -r abdf38ee314a -r 9acd819db33a src/Tools/Graphview/model.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)) } } diff -r abdf38ee314a -r 9acd819db33a src/Tools/Graphview/mutator_dialog.scala --- 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 = { diff -r abdf38ee314a -r 9acd819db33a src/Tools/Graphview/mutator_event.scala --- 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