changeset 59233 | 876a81f5788b |
parent 59228 | 56b34fc7a015 |
child 59240 | e411afcfaa29 |
--- a/src/Tools/Graphview/main_panel.scala Thu Jan 01 21:01:18 2015 +0100 +++ b/src/Tools/Graphview/main_panel.scala Thu Jan 01 21:09:07 2015 +0100 @@ -25,8 +25,7 @@ focusable = true requestFocus() - def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String = null - val graph_panel = new Graph_Panel(visualizer, make_tooltip) + val graph_panel = new Graph_Panel(visualizer) listenTo(keys) reactions += graph_panel.reactions