tuned window position;
authorwenzelm
Fri, 05 Oct 2012 12:00:28 +0200
changeset 49708 295ec55e7baa
parent 49707 e42f60561aa4
child 49709 3062937b45b3
tuned window position;
src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Fri Oct 05 11:36:46 2012 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Fri Oct 05 12:00:28 2012 +0200
@@ -26,15 +26,6 @@
 {
   window =>
 
-  private val point = {
-    val painter = text_area.getPainter
-    val fm = painter.getFontMetrics
-    val bounds = painter.getBounds()
-    val point = new Point(bounds.x + x, bounds.y + fm.getHeight + y)
-    SwingUtilities.convertPointToScreen(point, painter)
-    point
-  }
-
   window.addWindowFocusListener(new WindowAdapter {
     override def windowLostFocus(e: WindowEvent) { window.dispose() }
   })
@@ -62,7 +53,14 @@
   pretty_text_area.update(rendering.snapshot, body)
 
   window.add(pretty_text_area)
-  window.setLocation(point.x, point.y)
+
+  {
+    val container = text_area.getPainter
+    val font_metrics = container.getFontMetrics
+    val point = new Point(x, y + font_metrics.getHeight / 2)
+    SwingUtilities.convertPointToScreen(point, container)
+    window.setLocation(point.x, point.y)
+  }
 
   {
     val font_metrics = pretty_text_area.getPainter.getFontMetrics