make it independent from GUI thread, e.g. for Graph_File.write;

--- a/src/Tools/Graphview/mutator_event.scala	Sun Jan 25 17:48:14 2015 +0100
+++ b/src/Tools/Graphview/mutator_event.scala	Sun Jan 25 18:31:35 2015 +0100
@@ -10,10 +10,6 @@
 
 import isabelle._
 
-import scala.collection.mutable
-
-import java.awt.Color
-
 
 object Mutator_Event
 {
@@ -25,10 +21,10 @@
 
   class Bus
   {
-    private val receivers = new mutable.ListBuffer[Receiver]
+    private val receivers = Synchronized(List.empty[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)) }
+    def += (r: Receiver) { receivers.change(Library.insert(r)) }
+    def -= (r: Receiver) { receivers.change(Library.remove(r)) }
+    def event(x: Message) { receivers.value.reverse.foreach(r => r(x)) }
   }
 }
\ No newline at end of file