--- 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><pre style=\"font-family: " + visualizer.font_family +
- "; font-size: " + visualizer.tooltip_font_size + "px; \">" +
- HTML.encode(Pretty.string_of(body)) + "</pre></html>"
-
+ 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)