diff -r fc2e3b9d4852 -r 44658062d822 src/Tools/Graphview/src/graph_panel.scala
--- a/src/Tools/Graphview/src/graph_panel.scala	Sat Oct 20 15:45:40 2012 +0200
+++ b/src/Tools/Graphview/src/graph_panel.scala	Sat Oct 20 15:46:48 2012 +0200
@@ -67,7 +67,7 @@
   
   def apply_layout() = visualizer.Coordinates.layout()  
 
-  private val paint_panel = new Panel {    
+  private class Paint_Panel extends Panel {
     def set_preferred_size() {
         val (minX, minY, maxX, maxY) = visualizer.Coordinates.bounds()
         val s = Transform.scale
@@ -86,6 +86,7 @@
       visualizer.Drawer.paint_all_visible(g, true)
     }
   }
+  private val paint_panel = new Paint_Panel
   contents = paint_panel
   
   listenTo(keys)