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}