# HG changeset patch
# User wenzelm
# Date 1730751926 -3600
# Node ID 1b9ea66810ffca2de86e93f1de424b01b835155b
# Parent  b5b0c398cdec9de5c6ff20dbb006b3b76cdd6b8b
tuned;

diff -r b5b0c398cdec -r 1b9ea66810ff src/Pure/GUI/font_metric.scala
--- a/src/Pure/GUI/font_metric.scala	Mon Nov 04 21:05:11 2024 +0100
+++ b/src/Pure/GUI/font_metric.scala	Mon Nov 04 21:25:26 2024 +0100
@@ -32,12 +32,12 @@
   def string_bounds(str: String): Rectangle2D = font.getStringBounds(str, context)
   def string_width(str: String): Double = string_bounds(str).getWidth
 
+  protected def sample: String = "mix"
+  val height: Double = string_bounds(sample).getHeight
+  val average_width: Double = string_width(sample) / sample.length
+
   val space_width: Double = string_width(Symbol.space)
   override def unit: Double = space_width max 1.0
   override def apply(s: String): Double = if (s == "\n") 1.0 else string_width(s) / unit
-
-  protected def sample: String = "mix"
-  val height: Double = string_bounds(sample).getHeight
-  val average_width: Double = string_bounds(sample).getWidth / sample.length
   def average: Double = average_width / unit
 }