diff -r 9863ddead037 -r ae5695161423 src/Pure/GUI/font_metric.scala
--- 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
 }