src/Tools/Graphview/graph_panel.scala
changeset 59228 56b34fc7a015
parent 59226 7b8c50be8d42
child 59231 6dea47cf6c6b
--- a/src/Tools/Graphview/graph_panel.scala	Thu Jan 01 14:53:57 2015 +0100
+++ b/src/Tools/Graphview/graph_panel.scala	Thu Jan 01 15:58:30 2015 +0100
@@ -30,7 +30,7 @@
     override def getToolTipText(event: java.awt.event.MouseEvent): String =
       node(Transform.pane_to_graph_coordinates(event.getPoint)) match {
         case Some(name) =>
-          visualizer.model.complete.get_node(name).content match {
+          visualizer.model.complete_graph.get_node(name).content match {
             case Nil => null
             case content => make_tooltip(panel.peer, event.getX, event.getY, content)
           }