src/Tools/jEdit/src/graphview_dockable.scala
changeset 51496 cb677987b7e3
parent 51449 8d6e478934dc
child 52480 6a762cda56bd
     1.1 --- a/src/Tools/jEdit/src/graphview_dockable.scala	Sat Mar 23 16:46:09 2013 +0100
     1.2 +++ b/src/Tools/jEdit/src/graphview_dockable.scala	Sat Mar 23 19:39:31 2013 +0100
     1.3 @@ -65,7 +65,8 @@
     1.4            override def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String =
     1.5            {
     1.6              val rendering = Rendering(snapshot, PIDE.options.value)
     1.7 -            Pretty_Tooltip(view, parent, rendering, x, y, Command.Results.empty, body)
     1.8 +            Pretty_Tooltip(view, parent, rendering, x, y, Command.Results.empty,
     1.9 +              Text.Range(-1), body)
    1.10              null
    1.11            }
    1.12          }