author | wenzelm |
Sat, 17 Jan 2015 23:12:02 +0100 | |
changeset 59386 | 32b162d1d9b5 |
parent 59385 | 4b26be511f72 |
child 59387 | d15a96149703 |
--- 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