diff -r 50a3d663333a -r abe4c7cdac0e src/Tools/Graphview/visualizer.scala
--- a/src/Tools/Graphview/visualizer.scala	Sat Jan 03 20:51:10 2015 +0100
+++ b/src/Tools/Graphview/visualizer.scala	Sat Jan 03 20:58:33 2015 +0100
@@ -184,18 +184,18 @@
 
   object Drawer
   {
-    def apply(g: Graphics2D, node: Graph_Display.Node): Unit =
-      if (!node.is_dummy) Shapes.Growing_Node.paint(g, visualizer, node)
+    def apply(gfx: Graphics2D, node: Graph_Display.Node): Unit =
+      if (!node.is_dummy) Shapes.Growing_Node.paint(gfx, visualizer, node)
 
-    def apply(g: Graphics2D, edge: Graph_Display.Edge, head: Boolean, dummies: Boolean): Unit =
-      Shapes.Cardinal_Spline_Edge.paint(g, visualizer, edge, head, dummies)
+    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(g: Graphics2D, dummies: Boolean)
+    def paint_all_visible(gfx: Graphics2D, dummies: Boolean)
     {
-      g.setFont(font)
-      g.setRenderingHints(rendering_hints)
-      model.visible_edges_iterator.foreach(apply(g, _, arrow_heads, dummies))
-      model.visible_nodes_iterator.foreach(apply(g, _))
+      gfx.setFont(font)
+      gfx.setRenderingHints(rendering_hints)
+      model.visible_edges_iterator.foreach(apply(gfx, _, arrow_heads, dummies))
+      model.visible_nodes_iterator.foreach(apply(gfx, _))
     }
 
     def shape(m: Visualizer.Metrics, node: Graph_Display.Node): Shape =