src/Pure/GUI/gui.scala
changeset 59286 ac74eedb910a
parent 59230 cae3ef2897f2
child 59671 9715eb8e9408
--- a/src/Pure/GUI/gui.scala	Mon Jan 05 11:15:30 2015 +0100
+++ b/src/Pure/GUI/gui.scala	Mon Jan 05 14:13:38 2015 +0100
@@ -218,14 +218,14 @@
   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 =
+  def imitate_font(font: Font, family: String, scale: Double = 1.0): Font =
   {
     val font1 = new Font(family, font.getStyle, font.getSize)
-    val size = line_metrics(font).getHeight.toDouble / line_metrics(font1).getHeight * font.getSize
-    font1.deriveFont((scale * size).toInt)
+    val rel_size = line_metrics(font).getHeight.toDouble / line_metrics(font1).getHeight
+    new Font(family, font.getStyle, (scale * rel_size * font.getSize).toInt)
   }
 
-  def imitate_font_css(family: String, font: Font, scale: Double = 1.0): String =
+  def imitate_font_css(font: Font, family: String, scale: Double = 1.0): String =
   {
     val font1 = new Font(family, font.getStyle, font.getSize)
     val rel_size = line_metrics(font).getHeight.toDouble / line_metrics(font1).getHeight