--- a/src/Tools/jEdit/src/graphview_dockable.scala Sat Mar 23 16:46:09 2013 +0100
+++ b/src/Tools/jEdit/src/graphview_dockable.scala Sat Mar 23 19:39:31 2013 +0100
@@ -65,7 +65,8 @@
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, body)
+ Pretty_Tooltip(view, parent, rendering, x, y, Command.Results.empty,
+ Text.Range(-1), body)
null
}
}