tuned;
authorwenzelm
Fri Nov 30 14:21:28 2018 +0100 (12 months ago)
changeset 6937653194e2a969d
parent 69375 f8a1f1d7dd62
child 69377 81ae5893c556
tuned;
src/Pure/GUI/gui.scala
     1.1 --- a/src/Pure/GUI/gui.scala	Fri Nov 30 13:20:38 2018 +0100
     1.2 +++ b/src/Pure/GUI/gui.scala	Fri Nov 30 14:21:28 2018 +0100
     1.3 @@ -215,6 +215,18 @@
     1.4    def line_metrics(font: Font): LineMetrics =
     1.5      font.getLineMetrics("", new FontRenderContext(null, false, false))
     1.6  
     1.7 +  def transform_font(font: Font, transform: AffineTransform): Font =
     1.8 +  {
     1.9 +    import scala.collection.JavaConversions._
    1.10 +    font.deriveFont(Map(TextAttribute.TRANSFORM -> new TransformAttribute(transform)))
    1.11 +  }
    1.12 +
    1.13 +  def font(family: String = Isabelle_Fonts.sans, size: Int = 1, bold: Boolean = false): Font =
    1.14 +    new Font(family, if (bold) Font.BOLD else Font.PLAIN, size)
    1.15 +
    1.16 +
    1.17 +  /* Isabelle fonts */
    1.18 +
    1.19    def imitate_font(font: Font,
    1.20      family: String = Isabelle_Fonts.sans,
    1.21      scale: Double = 1.0): Font =
    1.22 @@ -232,14 +244,4 @@
    1.23      val rel_size = line_metrics(font).getHeight.toDouble / line_metrics(font1).getHeight
    1.24      "font-family: " + family + "; font-size: " + (scale * rel_size * 100).toInt + "%;"
    1.25    }
    1.26 -
    1.27 -  def transform_font(font: Font, transform: AffineTransform): Font =
    1.28 -  {
    1.29 -    import scala.collection.JavaConversions._
    1.30 -    font.deriveFont(Map(TextAttribute.TRANSFORM -> new TransformAttribute(transform)))
    1.31 -  }
    1.32 -
    1.33 -  def font(family: String = Isabelle_Fonts.sans, size: Int = 1, bold: Boolean = false): Font =
    1.34 -    new Font(family, if (bold) Font.BOLD else Font.PLAIN, size)
    1.35  }
    1.36 -