--- a/src/Tools/Graphview/graph_file.scala Wed Jan 28 19:15:13 2015 +0100
+++ b/src/Tools/Graphview/graph_file.scala Wed Jan 28 19:18:08 2015 +0100
@@ -26,7 +26,7 @@
gfx.setColor(Color.WHITE)
gfx.fillRect(0, 0, w, h)
gfx.translate(- box.x, - box.y)
- graphview.paint_all_visible(gfx)
+ graphview.paint(gfx)
}
val name = file.getName
--- a/src/Tools/Graphview/graph_panel.scala Wed Jan 28 19:15:13 2015 +0100
+++ b/src/Tools/Graphview/graph_panel.scala Wed Jan 28 19:18:08 2015 +0100
@@ -40,7 +40,7 @@
gfx.fillRect(0, 0, peer.getWidth, peer.getHeight)
gfx.transform(Transform())
- graphview.paint_all_visible(gfx)
+ graphview.paint(gfx)
}
}
--- a/src/Tools/Graphview/graphview.scala Wed Jan 28 19:15:13 2015 +0100
+++ b/src/Tools/Graphview/graphview.scala Wed Jan 28 19:18:08 2015 +0100
@@ -135,7 +135,7 @@
}
}
- def paint_all_visible(gfx: Graphics2D)
+ def paint(gfx: Graphics2D)
{
gfx.setRenderingHints(Metrics.rendering_hints)