src/Tools/Graphview/graph_panel.scala

--- a/src/Tools/Graphview/graph_panel.scala	Thu Jan 01 21:01:18 2015 +0100
+++ b/src/Tools/Graphview/graph_panel.scala	Thu Jan 01 21:09:07 2015 +0100
@@ -19,10 +19,7 @@
   MouseMoved, MouseClicked, MouseWheelMoved, MouseEvent}
 
 
-class Graph_Panel(
-    val visualizer: Visualizer,
-    make_tooltip: (JComponent, Int, Int, XML.Body) => String)
-  extends ScrollPane
+class Graph_Panel(val visualizer: Visualizer) extends ScrollPane
 {
   panel =>
 
@@ -32,7 +29,7 @@
         case Some(name) =>
           visualizer.model.complete_graph.get_node(name).content match {
             case Nil => null
-            case content => make_tooltip(panel.peer, event.getX, event.getY, content)
+            case content => visualizer.make_tooltip(panel.peer, event.getX, event.getY, content)
           }
         case None => null
       }