proper line height and text base line, like regular TextAreaPainter.PaintText;
authorwenzelm
Wed, 22 Oct 2014 17:34:01 +0200
changeset 58767 30766b5fd0e1
parent 58766 5bab56d3dcd4
child 58768 06dfbfa4b3ea
proper line height and text base line, like regular TextAreaPainter.PaintText;
src/Tools/jEdit/src/completion_popup.scala
src/Tools/jEdit/src/pretty_tooltip.scala
src/Tools/jEdit/src/rich_text_area.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 =
--- 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) })
--- 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)