tuned signature;

--- 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
           }
         }

--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Sat Jun 29 17:39:27 2013 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Sat Jun 29 18:20:09 2013 +0200
@@ -42,7 +42,6 @@
     rendering: Rendering,
     mouse_x: Int, mouse_y: Int,
     results: Command.Results,
-    range: Text.Range,
     body: XML.Body): Pretty_Tooltip =
   {
     Swing_Thread.require()
@@ -54,7 +53,7 @@
       }
     old.foreach(_.hide_popup)
 
-    val tip = new Pretty_Tooltip(view, rendering, parent, mouse_x, mouse_y, results, range, body)
+    val tip = new Pretty_Tooltip(view, rendering, parent, mouse_x, mouse_y, results, body)
     stack = tip :: rest
     tip
   }
@@ -129,7 +128,6 @@
   parent: JComponent,
   mouse_x: Int, mouse_y: Int,
   results: Command.Results,
-  range: Text.Range,
   body: XML.Body) extends JPanel(new BorderLayout)
 {
   tip =>

--- a/src/Tools/jEdit/src/rich_text_area.scala	Sat Jun 29 17:39:27 2013 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Sat Jun 29 18:20:09 2013 +0200
@@ -224,7 +224,7 @@
                     val painter = text_area.getPainter
                     val y1 = y + painter.getFontMetrics.getHeight / 2
                     val results = rendering.command_results(range)
-                    Pretty_Tooltip(view, painter, rendering, x, y1, results, tip.range, tip.info)
+                    Pretty_Tooltip(view, painter, rendering, x, y1, results, tip.info)
                 }
             }
           }