# HG changeset patch
# User wenzelm
# Date 1349431228 -7200
# Node ID 295ec55e7baa73bb873fc7eff41e20bc9dcdcc2a
# Parent  e42f60561aa4a76191d66461387a03e86eff8b84
tuned window position;

diff -r e42f60561aa4 -r 295ec55e7baa 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