--- a/src/Pure/GUI/font_metric.scala Wed Nov 06 11:05:18 2024 +0100
+++ b/src/Pure/GUI/font_metric.scala Wed Nov 06 15:17:39 2024 +0100
@@ -45,6 +45,13 @@
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
+ override def apply(s: String): Double = {
+ val s1 =
+ if (s.exists(c => Symbol.is_ascii_blank(c) && c != Symbol.space_char)) {
+ s.map(c => if (Symbol.is_ascii_blank(c)) Symbol.space_char else c)
+ }
+ else s
+ string_width(s1) / unit
+ }
def average: Double = average_width / unit
}