# HG changeset patch
# User wenzelm
# Date 1372534104 -7200
# Node ID 478ef4fa3d5a65b0d76497304ca5d72aa1b7abcb
# Parent  5b7c4fb41511073faf94a608df12ac5b76c52c73
more direct use of screen location: avoid misplacement if parent component has already disappeared asynchronously;

diff -r 5b7c4fb41511 -r 478ef4fa3d5a src/Tools/jEdit/src/graphview_dockable.scala
--- 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
           }
         }
diff -r 5b7c4fb41511 -r 478ef4fa3d5a src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Sat Jun 29 20:40:08 2013 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Sat Jun 29 21:28:24 2013 +0200
@@ -11,7 +11,7 @@
 
 import java.awt.{Color, Point, BorderLayout, Dimension}
 import java.awt.event.{FocusAdapter, FocusEvent}
-import javax.swing.{SwingUtilities, JWindow, JPanel, JComponent, PopupFactory}
+import javax.swing.{JWindow, JPanel, JComponent, PopupFactory}
 import javax.swing.border.LineBorder
 
 import scala.swing.{FlowPanel, Label}
@@ -40,7 +40,7 @@
     view: View,
     parent: JComponent,
     rendering: Rendering,
-    mouse_x: Int, mouse_y: Int,
+    screen_point: Point,
     results: Command.Results,
     body: XML.Body): Pretty_Tooltip =
   {
@@ -53,7 +53,7 @@
       }
     old.foreach(_.hide_popup)
 
-    val tip = new Pretty_Tooltip(view, rendering, parent, mouse_x, mouse_y, results, body)
+    val tip = new Pretty_Tooltip(view, rendering, parent, screen_point, results, body)
     stack = tip :: rest
     tip
   }
@@ -126,7 +126,7 @@
   view: View,
   rendering: Rendering,
   parent: JComponent,
-  mouse_x: Int, mouse_y: Int,
+  screen_point: Point,
   results: Command.Results,
   body: XML.Body) extends JPanel(new BorderLayout)
 {
@@ -194,8 +194,6 @@
 
   private val popup =
   {
-    val screen_point = new Point(mouse_x, mouse_y)
-    SwingUtilities.convertPointToScreen(screen_point, parent)
     val screen_bounds = JEdit_Lib.screen_bounds(screen_point)
 
     val painter = pretty_text_area.getPainter
diff -r 5b7c4fb41511 -r 478ef4fa3d5a src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Sat Jun 29 20:40:08 2013 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Sat Jun 29 21:28:24 2013 +0200
@@ -224,9 +224,10 @@
                   case None =>
                   case Some(tip) =>
                     val painter = text_area.getPainter
-                    val y1 = y + painter.getFontMetrics.getHeight / 2
+                    val screen_point = e.getLocationOnScreen
+                    screen_point.translate(0, painter.getFontMetrics.getHeight / 2)
                     val results = rendering.command_results(range)
-                    Pretty_Tooltip(view, painter, rendering, x, y1, results, tip.info)
+                    Pretty_Tooltip(view, painter, rendering, screen_point, results, tip.info)
                 }
             }
           }