--- 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)