1/*  Title:      Tools/Graphview/mutator_event.scala
2    Author:     Markus Kaiser, TU Muenchen
3    Author:     Makarius
4
5Events for dialog synchronization.
6*/
7
8package isabelle.graphview
9
10
11import isabelle._
12
13
14object Mutator_Event
15{
16  sealed abstract class Message
17  case class Add(m: Mutator.Info) extends Message
18  case class New_List(m: List[Mutator.Info]) extends Message
19
20  type Receiver = PartialFunction[Message, Unit]
21
22  class Bus
23  {
24    private val receivers = Synchronized[List[Receiver]](Nil)
25
26    def += (r: Receiver) { receivers.change(Library.insert(r)) }
27    def -= (r: Receiver) { receivers.change(Library.remove(r)) }
28    def event(x: Message) { receivers.value.reverse.foreach(r => r(x)) }
29  }
30}