--- a/src/Tools/jEdit/src/graphview_dockable.scala Sat Jun 29 17:39:27 2013 +0200
+++ b/src/Tools/jEdit/src/graphview_dockable.scala Sat Jun 29 18:20:09 2013 +0200
@@ -65,8 +65,7 @@
override def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String =
{
val rendering = Rendering(snapshot, PIDE.options.value)
- Pretty_Tooltip(view, parent, rendering, x, y, Command.Results.empty,
- Text.Range(-1), body)
+ Pretty_Tooltip(view, parent, rendering, x, y, Command.Results.empty, body)
null
}
}