src/Tools/jEdit/src/graphview_dockable.scala
changeset 52480 6a762cda56bd
parent 51496 cb677987b7e3
child 52483 478ef4fa3d5a
     1.1 --- a/src/Tools/jEdit/src/graphview_dockable.scala	Sat Jun 29 17:39:27 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/graphview_dockable.scala	Sat Jun 29 18:20:09 2013 +0200
     1.3 @@ -65,8 +65,7 @@
     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,
     1.8 -              Text.Range(-1), body)
     1.9 +            Pretty_Tooltip(view, parent, rendering, x, y, Command.Results.empty, body)
    1.10              null
    1.11            }
    1.12          }