# HG changeset patch
# User wenzelm
# Date 1372522809 -7200
# Node ID 6a762cda56bddfddad40b0e2a1e959d39823b071
# Parent  bb516d01d2595b36cb06c4165792adbaa32b7ea5
tuned signature;

diff -r bb516d01d259 -r 6a762cda56bd src/Tools/jEdit/src/graphview_dockable.scala
--- 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
           }
         }
diff -r bb516d01d259 -r 6a762cda56bd src/Tools/jEdit/src/pretty_tooltip.scala
--- 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 =>
diff -r bb516d01d259 -r 6a762cda56bd src/Tools/jEdit/src/rich_text_area.scala
--- 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)
                 }
             }
           }