# HG changeset patch
# User wenzelm
# Date 1421532722 -3600
# Node ID 32b162d1d9b517f0c83d5aa6feab11cfb7ad7a4f
# Parent  4b26be511f72bec6f7753f4efc5bc49435c546a3
proper refresh after apply_layout, in order to update preferred size, which is required for scroll pane;

diff -r 4b26be511f72 -r 32b162d1d9b5 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