src/Tools/jEdit/src/token_markup.scala
changeset 59230 cae3ef2897f2
parent 59083 88b0b1f28adc
child 59286 ac74eedb910a
--- a/src/Tools/jEdit/src/token_markup.scala	Thu Jan 01 16:08:12 2015 +0100
+++ b/src/Tools/jEdit/src/token_markup.scala	Thu Jan 01 17:27:52 2015 +0100
@@ -90,8 +90,8 @@
         def shift(y: Float): Font =
           GUI.transform_font(font1, AffineTransform.getTranslateInstance(0.0, y.toDouble))
 
-        val m0 = GUI.font_metrics(font0)
-        val m1 = GUI.font_metrics(font1)
+        val m0 = GUI.line_metrics(font0)
+        val m1 = GUI.line_metrics(font1)
         val a = m1.getAscent - m0.getAscent
         val b = (m1.getDescent + m1.getLeading) - (m0.getDescent + m0.getLeading)
         if (a > 0.0f) shift(a)