# HG changeset patch
# User wenzelm
# Date 1414012540 -7200
# Node ID 06dfbfa4b3eab4b1d4c03ecc328334d082f36899
# Parent  c0e46e1beefc6b2e06aca91bcceef3a0fba3f4bc# Parent  30766b5fd0e1f49d6ab57b59d8d32180de23c247
merged

diff -r c0e46e1beefc -r 06dfbfa4b3ea src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Wed Oct 22 17:34:19 2014 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala	Wed Oct 22 23:15:40 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 c0e46e1beefc -r 06dfbfa4b3ea src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Wed Oct 22 17:34:19 2014 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Wed Oct 22 23:15:40 2014 +0200
@@ -10,7 +10,7 @@
 
 import isabelle._
 
-import java.awt.{Color, Font, FontMetrics, Toolkit, Window}
+import java.awt.{Color, Font, Toolkit, Window}
 import java.awt.event.KeyEvent
 import javax.swing.JTextField
 import javax.swing.event.{DocumentListener, DocumentEvent}
diff -r c0e46e1beefc -r 06dfbfa4b3ea src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Wed Oct 22 17:34:19 2014 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Wed Oct 22 23:15:40 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 c0e46e1beefc -r 06dfbfa4b3ea src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Wed Oct 22 17:34:19 2014 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Wed Oct 22 23:15:40 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)