src/Tools/Graphview/graph_panel.scala

 import scala.swing.{Panel, ScrollPane}
 import scala.swing.event.{Event, Key, KeyTyped, MousePressed, MouseDragged,
   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 =>
 
   override lazy val peer: JScrollPane = new JScrollPane with SuperMixin {
     override def getToolTipText(event: java.awt.event.MouseEvent): String =
       node(Transform.pane_to_graph_coordinates(event.getPoint)) match {
         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
       }
   }