changeset 59397 | fc909f7e7ce5 |
parent 59396 | a2f4252c5489 |
child 59400 | d833cba5cce5 |
--- a/src/Tools/Graphview/main_panel.scala Sun Jan 18 20:15:05 2015 +0100 +++ b/src/Tools/Graphview/main_panel.scala Sun Jan 18 21:35:54 2015 +0100 @@ -21,14 +21,8 @@ class Main_Panel(model: Model, visualizer: Visualizer) extends BorderPanel { - private def repaint_all() - { - revalidate() - repaint() - } - val graph_panel = new Graph_Panel(visualizer) - val tree_panel = new Tree_Panel(visualizer, repaint_all _) + val tree_panel = new Tree_Panel(visualizer, graph_panel) def update_layout() {