src/Tools/Graphview/mutator_event.scala
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (3 months ago)
changeset 69981 3dced198b9ec
parent 61590 94ab348eaab2
permissions -rw-r--r--
more strict AFP properties;
     1 /*  Title:      Tools/Graphview/mutator_event.scala
     2     Author:     Markus Kaiser, TU Muenchen
     3     Author:     Makarius
     4 
     5 Events for dialog synchronization.
     6 */
     7 
     8 package isabelle.graphview
     9 
    10 
    11 import isabelle._
    12 
    13 
    14 object 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 }