src/Tools/Graphview/src/mutator_event.scala
changeset 59202 711c2446dc9d
parent 59201 702e0971d617
child 59203 5f0bd5afc16d
--- 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