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