# 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 }