# HG changeset patch
# User wenzelm
# Date 1543584088 -3600
# Node ID 53194e2a969d9c2b44f554f01ee9d691bfe5ce71
# Parent  f8a1f1d7dd62fb5cbb0dbb3d55ec3d36c010144e
tuned;

diff -r f8a1f1d7dd62 -r 53194e2a969d src/Pure/GUI/gui.scala
--- a/src/Pure/GUI/gui.scala	Fri Nov 30 13:20:38 2018 +0100
+++ b/src/Pure/GUI/gui.scala	Fri Nov 30 14:21:28 2018 +0100
@@ -215,6 +215,18 @@
   def line_metrics(font: Font): LineMetrics =
     font.getLineMetrics("", new FontRenderContext(null, false, false))
 
+  def transform_font(font: Font, transform: AffineTransform): Font =
+  {
+    import scala.collection.JavaConversions._
+    font.deriveFont(Map(TextAttribute.TRANSFORM -> new TransformAttribute(transform)))
+  }
+
+  def font(family: String = Isabelle_Fonts.sans, size: Int = 1, bold: Boolean = false): Font =
+    new Font(family, if (bold) Font.BOLD else Font.PLAIN, size)
+
+
+  /* Isabelle fonts */
+
   def imitate_font(font: Font,
     family: String = Isabelle_Fonts.sans,
     scale: Double = 1.0): Font =
@@ -232,14 +244,4 @@
     val rel_size = line_metrics(font).getHeight.toDouble / line_metrics(font1).getHeight
     "font-family: " + family + "; font-size: " + (scale * rel_size * 100).toInt + "%;"
   }
-
-  def transform_font(font: Font, transform: AffineTransform): Font =
-  {
-    import scala.collection.JavaConversions._
-    font.deriveFont(Map(TextAttribute.TRANSFORM -> new TransformAttribute(transform)))
-  }
-
-  def font(family: String = Isabelle_Fonts.sans, size: Int = 1, bold: Boolean = false): Font =
-    new Font(family, if (bold) Font.BOLD else Font.PLAIN, size)
 }
-