diff -r 19b5fc4b2b38 -r be4180f3c236 src/Tools/Graphview/visualizer.scala
--- a/src/Tools/Graphview/visualizer.scala	Sat Jan 03 15:45:01 2015 +0100
+++ b/src/Tools/Graphview/visualizer.scala	Sat Jan 03 20:22:27 2015 +0100
@@ -105,21 +105,18 @@
   {
     private var layout = Layout.empty
 
-    def apply(k: String): (Double, Double) =
-      layout.nodes.getOrElse(k, (0.0, 0.0))
+    def apply(node: Graph_Display.Node): (Double, Double) =
+      layout.nodes.getOrElse(node, (0.0, 0.0))
 
-    def apply(e: (String, String)): List[(Double, Double)] =
-      layout.dummies.get(e) match {
-        case Some(ds) => ds
-        case None => Nil
-      }
+    def apply(edge: Graph_Display.Edge): List[(Double, Double)] =
+      layout.dummies.getOrElse(edge, Nil)
 
-    def reposition(k: String, to: (Double, Double))
+    def reposition(node: Graph_Display.Node, to: (Double, Double))
     {
-      layout = layout.copy(nodes = layout.nodes + (k -> to))
+      layout = layout.copy(nodes = layout.nodes + (node -> to))
     }
 
-    def reposition(d: ((String, String), Int), to: (Double, Double))
+    def reposition(d: (Graph_Display.Edge, Int), to: (Double, Double))
     {
       val (e, index) = d
       layout.dummies.get(e) match {
@@ -133,15 +130,15 @@
       }
     }
 
-    def translate(k: String, by: (Double, Double))
+    def translate(node: Graph_Display.Node, by: (Double, Double))
     {
-      val ((x, y), (dx, dy)) = (Coordinates(k), by)
-      reposition(k, (x + dx, y + dy))
+      val ((x, y), (dx, dy)) = (Coordinates(node), by)
+      reposition(node, (x + dx, y + dy))
     }
 
-    def translate(d: ((String, String), Int), by: (Double, Double))
+    def translate(d: (Graph_Display.Edge, Int), by: (Double, Double))
     {
-      val ((e, i),(dx, dy)) = (d, by)
+      val ((e, i), (dx, dy)) = (d, by)
       val (x, y) = apply(e)(i)
       reposition(d, (x + dx, y + dy))
     }
@@ -154,8 +151,8 @@
           val m = metrics()
 
           val max_width =
-            model.current_graph.iterator.map({ case (_, (info, _)) =>
-              m.string_bounds(info.name).getWidth }).max
+            model.current_graph.keys_iterator.map(
+              node => m.string_bounds(node.toString).getWidth).max
           val box_distance = (max_width + m.pad + m.gap).ceil
           def box_height(n: Int): Double = (m.char_width * 1.5 * (5 max n)).ceil
 
@@ -170,8 +167,8 @@
       var y0 = 0.0
       var x1 = 0.0
       var y1 = 0.0
-      for (node_name <- model.visible_nodes_iterator) {
-        val shape = Shapes.Growing_Node.shape(m, visualizer, Some(node_name))
+      for (node <- model.visible_nodes_iterator) {
+        val shape = Shapes.Growing_Node.shape(m, visualizer, node)
         x0 = x0 min shape.getMinX
         y0 = y0 min shape.getMinY
         x1 = x1 max shape.getMaxX
@@ -187,67 +184,46 @@
 
   object Drawer
   {
-    def apply(g: Graphics2D, n: Option[String])
-    {
-      n match {
-        case None =>
-        case Some(_) => Shapes.Growing_Node.paint(g, visualizer, n)
-      }
-    }
+    def apply(g: Graphics2D, node: Graph_Display.Node): Unit =
+      if (!node.is_dummy) Shapes.Growing_Node.paint(g, visualizer, node)
 
-    def apply(g: Graphics2D, e: (String, String), head: Boolean, dummies: Boolean)
-    {
-      Shapes.Cardinal_Spline_Edge.paint(g, visualizer, e, head, dummies)
-    }
+    def apply(g: Graphics2D, edge: Graph_Display.Edge, head: Boolean, dummies: Boolean): Unit =
+      Shapes.Cardinal_Spline_Edge.paint(g, visualizer, edge, head, dummies)
 
     def paint_all_visible(g: Graphics2D, dummies: Boolean)
     {
       g.setFont(font)
-
       g.setRenderingHints(rendering_hints)
-
-      model.visible_edges_iterator.foreach(e => {
-          apply(g, e, arrow_heads, dummies)
-        })
-
-      model.visible_nodes_iterator.foreach(l => {
-          apply(g, Some(l))
-        })
+      model.visible_edges_iterator.foreach(apply(g, _, arrow_heads, dummies))
+      model.visible_nodes_iterator.foreach(apply(g, _))
     }
 
-    def shape(m: Visualizer.Metrics, n: Option[String]): Shape =
-      if (n.isEmpty) Shapes.Dummy.shape(m, visualizer, n)
-      else Shapes.Growing_Node.shape(m, visualizer, n)
+    def shape(m: Visualizer.Metrics, node: Graph_Display.Node): Shape =
+      if (node.is_dummy) Shapes.Dummy.shape(m, visualizer, node)
+      else Shapes.Growing_Node.shape(m, visualizer, node)
   }
 
   object Selection
   {
-    private var selected: List[String] = Nil
+    // owned by GUI thread
+    private var state: List[Graph_Display.Node] = Nil
 
-    def apply() = selected
-    def apply(s: String) = selected.contains(s)
+    def get(): List[Graph_Display.Node] = GUI_Thread.require { state }
+    def contains(node: Graph_Display.Node): Boolean = get().contains(node)
 
-    def add(s: String) { selected = s :: selected }
-    def set(ss: List[String]) { selected = ss }
-    def clear() { selected = Nil }
+    def add(node: Graph_Display.Node): Unit = GUI_Thread.require { state = node :: state }
+    def clear(): Unit = GUI_Thread.require { state = Nil }
   }
 
   sealed case class Node_Color(border: Color, background: Color, foreground: Color)
 
-  def node_color(l: Option[String]): Node_Color =
-    l match {
-      case None =>
-        Node_Color(foreground1_color, background_color, foreground_color)
-      case Some(c) if Selection(c) =>
-        Node_Color(foreground_color, selection_color, foreground_color)
-      case Some(c) =>
-        Node_Color(foreground_color, model.colors.getOrElse(c, background_color), foreground_color)
-    }
+  def node_color(node: Graph_Display.Node): Node_Color =
+    if (node.is_dummy)
+      Node_Color(foreground1_color, background_color, foreground_color)
+    else if (Selection.contains(node))
+      Node_Color(foreground_color, selection_color, foreground_color)
+    else
+      Node_Color(foreground_color, model.colors.getOrElse(node, background_color), foreground_color)
 
-  def edge_color(e: (String, String)): Color = foreground_color
-
-  object Caption
-  {
-    def apply(key: String) = model.complete_graph.get_node(key).name
-  }
+  def edge_color(edge: Graph_Display.Edge): Color = foreground_color
 }
\ No newline at end of file