# HG changeset patch
# User wenzelm
# Date 1422207095 -3600
# Node ID 9f45b95d35435a1ab3a50fa4fa799e8c9a1f04b8
# Parent  ab2c3597f1d3924b16ca67ef89e2a3ca95261e16
make it independent from GUI thread, e.g. for Graph_File.write;

diff -r ab2c3597f1d3 -r 9f45b95d3543 src/Tools/Graphview/mutator_event.scala
--- 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