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