diff -r 305e79989d48 -r 126293918a37 src/Tools/Graphview/visualizer.scala
--- a/src/Tools/Graphview/visualizer.scala	Mon Jan 05 23:05:17 2015 +0100
+++ b/src/Tools/Graphview/visualizer.scala	Mon Jan 05 23:29:38 2015 +0100
@@ -52,7 +52,9 @@
 
   /* rendering parameters */
 
+  // owned by GUI thread
   var arrow_heads = false
+  var show_dummies = false
 
   object Colors
   {
@@ -74,6 +76,14 @@
     }
   }
 
+  def paint_all_visible(gfx: Graphics2D)
+  {
+    gfx.setRenderingHints(Metrics.rendering_hints)
+    for (edge <- visible_graph.edges_iterator)
+      Shapes.Cardinal_Spline_Edge.paint(gfx, visualizer, edge)
+    for (node <- visible_graph.keys_iterator)
+      Shapes.Node.paint(gfx, visualizer, node)
+  }
 
   object Coordinates
   {
@@ -129,22 +139,6 @@
     }
   }
 
-  object Drawer
-  {
-    def apply(gfx: Graphics2D, node: Graph_Display.Node): Unit =
-      if (!node.is_dummy) Shapes.Node.paint(gfx, visualizer, node)
-
-    def apply(gfx: Graphics2D, edge: Graph_Display.Edge, head: Boolean, dummies: Boolean): Unit =
-      Shapes.Cardinal_Spline_Edge.paint(gfx, visualizer, edge, head, dummies)
-
-    def paint_all_visible(gfx: Graphics2D, dummies: Boolean)
-    {
-      gfx.setRenderingHints(Metrics.rendering_hints)
-      visible_graph.edges_iterator.foreach(apply(gfx, _, arrow_heads, dummies))
-      visible_graph.keys_iterator.foreach(apply(gfx, _))
-    }
-  }
-
   object Selection
   {
     // owned by GUI thread