# HG changeset patch
# User wenzelm
# Date 1420129672 -3600
# Node ID cae3ef2897f2ff00067b5a584ec5e52ddcbca9f5
# Parent  7b4b025b05995e2b9d5e90af3afb1d1d9ea92402
tuned signature;

diff -r 7b4b025b0599 -r cae3ef2897f2 src/Pure/GUI/gui.scala
--- a/src/Pure/GUI/gui.scala	Thu Jan 01 16:08:12 2015 +0100
+++ b/src/Pure/GUI/gui.scala	Thu Jan 01 17:27:52 2015 +0100
@@ -215,20 +215,20 @@
 
   /* font operations */
 
-  def font_metrics(font: Font): LineMetrics =
+  def line_metrics(font: Font): LineMetrics =
     font.getLineMetrics("", new FontRenderContext(null, false, false))
 
   def imitate_font(family: String, font: Font, scale: Double = 1.0): Font =
   {
     val font1 = new Font(family, font.getStyle, font.getSize)
-    val size = font_metrics(font).getHeight.toDouble / font_metrics(font1).getHeight * font.getSize
+    val size = line_metrics(font).getHeight.toDouble / line_metrics(font1).getHeight * font.getSize
     font1.deriveFont((scale * size).toInt)
   }
 
   def imitate_font_css(family: String, font: Font, scale: Double = 1.0): String =
   {
     val font1 = new Font(family, font.getStyle, font.getSize)
-    val rel_size = font_metrics(font).getHeight.toDouble / font_metrics(font1).getHeight
+    val rel_size = line_metrics(font).getHeight.toDouble / line_metrics(font1).getHeight
     "font-family: " + family + "; font-size: " + (scale * rel_size * 100).toInt + "%;"
   }
 
diff -r 7b4b025b0599 -r cae3ef2897f2 src/Tools/jEdit/src/token_markup.scala
--- 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)