diff -r 6e10bf974693 -r e865c4d99c49 src/Tools/Graphview/src/main_panel.scala --- a/src/Tools/Graphview/src/main_panel.scala Wed May 21 12:34:27 2014 +0200 +++ b/src/Tools/Graphview/src/main_panel.scala Wed May 21 12:49:27 2014 +0200 @@ -32,11 +32,7 @@ val model = new Model(graph) val visualizer = new Visualizer(model) - def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String = - "

" +
-      HTML.encode(Pretty.string_of(body)) + "

" - + def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String = null val graph_panel = new Graph_Panel(visualizer, make_tooltip) listenTo(keys)