proper refresh after apply_layout, in order to update preferred size, which is required for scroll pane;
authorwenzelm
Sat, 17 Jan 2015 23:12:02 +0100
changeset 59386 32b162d1d9b5
parent 59385 4b26be511f72
child 59387 d15a96149703
proper refresh after apply_layout, in order to update preferred size, which is required for scroll pane;
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