equal
deleted
inserted
replaced
20 |
20 |
21 |
21 |
22 class Graph_Panel(val visualizer: Visualizer) extends ScrollPane |
22 class Graph_Panel(val visualizer: Visualizer) extends ScrollPane |
23 { |
23 { |
24 panel => |
24 panel => |
|
25 |
|
26 tooltip = "" |
25 |
27 |
26 override lazy val peer: JScrollPane = new JScrollPane with SuperMixin { |
28 override lazy val peer: JScrollPane = new JScrollPane with SuperMixin { |
27 override def getToolTipText(event: java.awt.event.MouseEvent): String = |
29 override def getToolTipText(event: java.awt.event.MouseEvent): String = |
28 node(Transform.pane_to_graph_coordinates(event.getPoint)) match { |
30 node(Transform.pane_to_graph_coordinates(event.getPoint)) match { |
29 case Some(name) => |
31 case Some(name) => |