diff -r 305e79989d48 -r 126293918a37 src/Tools/Graphview/main_panel.scala
--- a/src/Tools/Graphview/main_panel.scala	Mon Jan 05 23:05:17 2015 +0100
+++ b/src/Tools/Graphview/main_panel.scala	Mon Jan 05 23:29:38 2015 +0100
@@ -43,6 +43,10 @@
         selected = visualizer.arrow_heads
         action = Action("Arrow heads") { visualizer.arrow_heads = selected; graph_panel.repaint() }
       },
+      new CheckBox() {
+        selected = visualizer.show_dummies
+        action = Action("Show dummies") { visualizer.show_dummies = selected; graph_panel.repaint() }
+      },
       new Button {
         action = Action("Save image") {
           chooser.showSaveDialog(this) match {
@@ -71,7 +75,7 @@
       gfx.setColor(Color.WHITE)
       gfx.fillRect(0, 0, w, h)
       gfx.translate(- box.x, - box.y)
-      visualizer.Drawer.paint_all_visible(gfx, false)
+      visualizer.paint_all_visible(gfx)
     }
 
     try {