--- a/src/Tools/jEdit/src/graphview_dockable.scala Sat Jun 29 20:40:08 2013 +0200
+++ b/src/Tools/jEdit/src/graphview_dockable.scala Sat Jun 29 21:28:24 2013 +0200
@@ -9,7 +9,8 @@
import isabelle._
-import javax.swing.JComponent
+import javax.swing.{SwingUtilities, JComponent}
+import java.awt.Point
import java.awt.event.{WindowFocusListener, WindowEvent}
import org.gjt.sp.jedit.View
@@ -65,7 +66,9 @@
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, body)
+ val screen_point = new Point(x, y)
+ SwingUtilities.convertPointToScreen(screen_point, parent)
+ Pretty_Tooltip(view, parent, rendering, screen_point, Command.Results.empty, body)
null
}
}