--- 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)