diff -r 702e0971d617 -r 711c2446dc9d src/Tools/Graphview/src/mutator_event.scala --- a/src/Tools/Graphview/src/mutator_event.scala Tue Dec 30 11:50:34 2014 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,35 +0,0 @@ -/* Title: Tools/Graphview/src/mutator_event.scala - Author: Markus Kaiser, TU Muenchen - -Events for dialog synchronization. -*/ - -package isabelle.graphview - - -import isabelle._ - -import scala.collection.mutable - -import java.awt.Color - - -object Mutator_Event -{ - type Mutator_Markup = (Boolean, Color, Mutator) - - sealed abstract class Message - case class Add(m: Mutator_Markup) extends Message - case class NewList(m: List[Mutator_Markup]) extends Message - - type Receiver = PartialFunction[Message, Unit] - - class Bus - { - private val receivers = new mutable.ListBuffer[Receiver] - - def += (r: Receiver) { GUI_Thread.require {}; receivers += r } - def -= (r: Receiver) { GUI_Thread.require {}; receivers -= r } - def event(x: Message) { GUI_Thread.require {}; receivers.foreach(r => r(x)) } - } -} \ No newline at end of file