src/Tools/Graphview/mutator_event.scala
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (2 months ago)
changeset 69981 3dced198b9ec
parent 61590 94ab348eaab2
permissions -rw-r--r--
more strict AFP properties;
wenzelm@59202
     1
/*  Title:      Tools/Graphview/mutator_event.scala
markus@49557
     2
    Author:     Markus Kaiser, TU Muenchen
wenzelm@59240
     3
    Author:     Makarius
markus@49557
     4
markus@49557
     5
Events for dialog synchronization.
markus@49557
     6
*/
markus@49557
     7
markus@49557
     8
package isabelle.graphview
markus@49557
     9
markus@49557
    10
wenzelm@49733
    11
import isabelle._
wenzelm@49733
    12
markus@49557
    13
markus@49557
    14
object Mutator_Event
markus@49557
    15
{
markus@49557
    16
  sealed abstract class Message
wenzelm@59221
    17
  case class Add(m: Mutator.Info) extends Message
wenzelm@59221
    18
  case class New_List(m: List[Mutator.Info]) extends Message
wenzelm@49733
    19
wenzelm@49733
    20
  type Receiver = PartialFunction[Message, Unit]
wenzelm@49733
    21
wenzelm@49733
    22
  class Bus
wenzelm@49733
    23
  {
wenzelm@61590
    24
    private val receivers = Synchronized[List[Receiver]](Nil)
wenzelm@49733
    25
wenzelm@59442
    26
    def += (r: Receiver) { receivers.change(Library.insert(r)) }
wenzelm@59442
    27
    def -= (r: Receiver) { receivers.change(Library.remove(r)) }
wenzelm@59442
    28
    def event(x: Message) { receivers.value.reverse.foreach(r => r(x)) }
wenzelm@49733
    29
  }
markus@49557
    30
}