src/Tools/Graphview/main_panel.scala
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()
   {