diff -r 702e0971d617 -r 711c2446dc9d src/Tools/Graphview/mutator_event.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Graphview/mutator_event.scala	Tue Dec 30 14:11:06 2014 +0100
@@ -0,0 +1,35 @@
+/*  Title:      Tools/Graphview/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