src/Tools/Graphview/graph_panel.scala

--- a/src/Tools/Graphview/graph_panel.scala	Sat Jan 17 22:52:45 2015 +0100
+++ b/src/Tools/Graphview/graph_panel.scala	Sat Jan 17 23:12:02 2015 +0100
@@ -52,7 +52,8 @@
     }
   }
 
-  def fit_to_window() = {
+  def fit_to_window()
+  {
     Transform.fit_to_window()
     refresh()
   }
@@ -69,7 +70,7 @@
   def apply_layout()
   {
     visualizer.update_layout()
-    repaint()
+    refresh()
   }
 
   private class Paint_Panel extends Panel