src/Tools/Graphview/mutator_event.scala
author Fabian Huch <huch@in.tum.de>
Tue, 22 Oct 2024 17:32:34 +0200
changeset 81224 6922f189cb43
parent 78616 9acd819db33a
permissions -rw-r--r--
update ci mail address;

/*  Title:      Tools/Graphview/mutator_event.scala
    Author:     Markus Kaiser, TU Muenchen
    Author:     Makarius

Events for dialog synchronization.
*/

package isabelle.graphview


import isabelle._


object Mutator_Event {
  enum Message {
    case Add(m: Mutator.Info) extends Message
    case New_List(m: List[Mutator.Info]) extends Message
  }

  type Receiver = Message => Unit

  class Bus {
    private val receivers = Synchronized[List[Receiver]](Nil)

    def += (r: Receiver): Unit = receivers.change(Library.insert(r))
    def -= (r: Receiver): Unit = receivers.change(Library.remove(r))
    def event(x: Message): Unit = receivers.value.reverse.foreach(r => r(x))
  }
}