# HG changeset patch
# User wenzelm
# Date 1413992041 -7200
# Node ID 30766b5fd0e1f49d6ab57b59d8d32180de23c247
# Parent  5bab56d3dcd4f002b800221583e15a4bdc37cc18
proper line height and text base line, like regular TextAreaPainter.PaintText;

diff -r 5bab56d3dcd4 -r 30766b5fd0e1 src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Wed Oct 22 17:30:58 2014 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala	Wed Oct 22 17:34:01 2014 +0200
@@ -303,7 +303,7 @@
         if (loc1 != null) {
           val loc2 =
             SwingUtilities.convertPoint(painter,
-              loc1.x, loc1.y + painter.getFontMetrics.getHeight, layered)
+              loc1.x, loc1.y + painter.getLineHeight, layered)
 
           val items = result.items.map(new Item(_))
           val completion =
diff -r 5bab56d3dcd4 -r 30766b5fd0e1 src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Wed Oct 22 17:30:58 2014 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Wed Oct 22 17:34:01 2014 +0200
@@ -264,7 +264,7 @@
         XML.traverse_text(formatted)(0)(
           (n: Int, s: String) => n + s.iterator.filter(_ == '\n').length)
 
-      val h = painter.getFontMetrics.getHeight * (lines + 1) + geometry.deco_height
+      val h = painter.getLineHeight * (lines + 1) + geometry.deco_height
       val margin1 =
         if (h <= h_max)
           (0.0 /: split_lines(XML.content(formatted)))({ case (m, line) => m max metric(line) })
diff -r 5bab56d3dcd4 -r 30766b5fd0e1 src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Wed Oct 22 17:30:58 2014 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Wed Oct 22 17:34:01 2014 +0200
@@ -251,7 +251,7 @@
                         case None =>
                         case Some(tip) =>
                           val painter = text_area.getPainter
-                          val loc = new Point(x, y + painter.getFontMetrics.getHeight / 2)
+                          val loc = new Point(x, y + painter.getLineHeight / 2)
                           val results = rendering.command_results(tip.range)
                           Pretty_Tooltip(view, painter, loc, rendering, results, tip)
                       }
@@ -444,7 +444,7 @@
 
         val clip = gfx.getClip
         val x0 = text_area.getHorizontalOffset
-        var y0 = y + fm.getHeight - (fm.getLeading + 1) - fm.getDescent
+        var y0 = y + painter.getLineHeight - (fm.getLeading + 1) - fm.getDescent
 
         val (bullet_x, bullet_y, bullet_w, bullet_h) =
         {
@@ -596,7 +596,7 @@
 
             val offset = caret - text_area.getLineStartOffset(physical_line)
             val x = text_area.offsetToXY(physical_line, offset).x
-            val y1 = y + fm.getHeight - (fm.getLeading + 1) - fm.getDescent
+            val y1 = y + painter.getLineHeight - (fm.getLeading + 1) - fm.getDescent
 
             val astr = new AttributedString(" ")
             astr.addAttribute(TextAttribute.FONT, painter.getFont)