src/Tools/Graphview/src/main_panel.scala
changeset 57035 e865c4d99c49
parent 50491 0faaa279faee
child 57044 042d6e58cb40
     1.1 --- a/src/Tools/Graphview/src/main_panel.scala	Wed May 21 12:34:27 2014 +0200
     1.2 +++ b/src/Tools/Graphview/src/main_panel.scala	Wed May 21 12:49:27 2014 +0200
     1.3 @@ -32,11 +32,7 @@
     1.4    val model = new Model(graph)
     1.5    val visualizer = new Visualizer(model)
     1.6  
     1.7 -  def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String =
     1.8 -    "<html><pre style=\"font-family: " + visualizer.font_family +
     1.9 -      "; font-size: " + visualizer.tooltip_font_size + "px; \">" +
    1.10 -      HTML.encode(Pretty.string_of(body)) + "</pre></html>"
    1.11 -
    1.12 +  def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String = null
    1.13    val graph_panel = new Graph_Panel(visualizer, make_tooltip)
    1.14  
    1.15    listenTo(keys)