prefer synchronous Mutator_Event.Bus on Swing_Thread;

--- a/src/Tools/Graphview/src/graph_panel.scala	Mon Oct 08 13:20:55 2012 +0200
+++ b/src/Tools/Graphview/src/graph_panel.scala	Mon Oct 08 14:10:38 2012 +0200
@@ -97,20 +97,9 @@
       case MouseClicked(_, _, _, _, _) => {repaint(); requestFocus()}
       case MouseMoved(_, _, _) => repaint()
     }
-  private val r = {
-    import scala.actors.Actor._
-    
-    actor {
-      loop {
-        react {
-          // FIXME Swing thread!?
-          case _ => repaint()
-        }
-      }
-    }
-  }
-  visualizer.model.Colors.events += r
-  visualizer.model.Mutators.events += r
+
+  visualizer.model.Colors.events += { case _ => repaint() }
+  visualizer.model.Mutators.events += { case _ => repaint() }
   
   apply_layout()
   fit_to_window()

--- a/src/Tools/Graphview/src/model.scala	Mon Oct 08 13:20:55 2012 +0200
+++ b/src/Tools/Graphview/src/model.scala	Mon Oct 08 14:10:38 2012 +0200
@@ -10,14 +10,12 @@
 import isabelle._
 import isabelle.graphview.Mutators._
 import java.awt.Color
-import scala.actors.Actor
-import scala.actors.Actor._
 
 
 class Mutator_Container(val available: List[Mutator]) {
     type Mutator_Markup = (Boolean, Color, Mutator)
     
-    val events = new Event_Bus[Mutator_Event.Message]
+    val events = new Mutator_Event.Bus
     
     private var _mutators : List[Mutator_Markup] = Nil
     def apply() = _mutators
@@ -103,11 +101,5 @@
           }
     })
   }
-  Colors.events += actor {
-    loop {
-      react {
-        case _ => build_colors()
-      }
-    }
-  }
+  Colors.events += { case _ => build_colors() }
 }
\ No newline at end of file

--- a/src/Tools/Graphview/src/mutator_dialog.scala	Mon Oct 08 13:20:55 2012 +0200
+++ b/src/Tools/Graphview/src/mutator_dialog.scala	Mon Oct 08 14:10:38 2012 +0200
@@ -14,16 +14,15 @@
 import javax.swing.border.EmptyBorder
 import scala.collection.JavaConversions._
 import scala.swing._
-import scala.actors.Actor
-import scala.actors.Actor._
 import isabelle.graphview.Mutators._
 import scala.swing.event.ValueChanged
 
 
 class Mutator_Dialog(
-  container: Mutator_Container, caption: String,
-  reverse_caption: String = "Inverse", show_color_chooser: Boolean = true)
-extends Dialog
+    container: Mutator_Container, caption: String,
+    reverse_caption: String = "Inverse",
+    show_color_chooser: Boolean = true)
+  extends Dialog
 {
   type Mutator_Markup = (Boolean, Color, Mutator)
   
@@ -36,15 +35,9 @@
     paintPanels
   }
 
-  container.events += actor {
-    loop {
-      react {
-        case Mutator_Event.Add(m) => addPanel(new Mutator_Panel(m))
-        case Mutator_Event.NewList(ms) => {
-            panels = getPanels(ms)
-        }
-      }
-    }
+  container.events += {
+    case Mutator_Event.Add(m) => addPanel(new Mutator_Panel(m))
+    case Mutator_Event.NewList(ms) => panels = getPanels(ms)
   }
 
   override def open() {

--- a/src/Tools/Graphview/src/mutator_event.scala	Mon Oct 08 13:20:55 2012 +0200
+++ b/src/Tools/Graphview/src/mutator_event.scala	Mon Oct 08 14:10:38 2012 +0200
@@ -7,14 +7,29 @@
 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) { Swing_Thread.require(); receivers += r }
+    def -= (r: Receiver) { Swing_Thread.require(); receivers -= r }
+    def event(x: Message) { Swing_Thread.require(); receivers.foreach(r => r(x)) }
+  }
 }
\ No newline at end of file