# HG changeset patch
# User wenzelm
# Date 1422469088 -3600
# Node ID 3a357fef24e80ad8691b319190c5b77382e8e212
# Parent  985fc55e9f272f08075c6908e88f818cdced03b8
tuned signature;

diff -r 985fc55e9f27 -r 3a357fef24e8 src/Tools/Graphview/graph_file.scala
--- 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
diff -r 985fc55e9f27 -r 3a357fef24e8 src/Tools/Graphview/graph_panel.scala
--- 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)
     }
   }
 
diff -r 985fc55e9f27 -r 3a357fef24e8 src/Tools/Graphview/graphview.scala
--- 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)