more robust and uniform metric, still with special treatment motivated by jEdit (see also 0cdfce0bf956);

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

--- a/src/Pure/General/symbol.ML	Wed Nov 06 11:05:18 2024 +0100
+++ b/src/Pure/General/symbol.ML	Wed Nov 06 15:17:39 2024 +0100
@@ -498,22 +498,22 @@
 
 (** symbol output **)
 
-(* length *)
+(* metric *)
 
-fun sym_len s =
+fun metric1 s =
   if String.isPrefix "\092<longlonglong" s then 4
   else if String.isPrefix "\092<longlong" s then 3
   else if String.isPrefix "\092<long" s orelse String.isPrefix "\092<Long" s then 2
-  else if is_printable s then 1
+  else if is_blank s orelse is_printable s then 1
   else 0;
 
-fun sym_length ss = fold (fn s => fn n => sym_len s + n) ss 0;
+fun metric ss = fold (fn s => fn n => metric1 s + n) ss 0;
 
-fun output s = (s, sym_length (Symbol.explode s));
+fun output s = (s, metric (Symbol.explode s));
 
 
 (*final declarations of this structure!*)
 val explode = Symbol.explode;
-val length = sym_length;
+val length = metric;
 
 end;

--- a/src/Pure/General/symbol.scala	Wed Nov 06 11:05:18 2024 +0100
+++ b/src/Pure/General/symbol.scala	Wed Nov 06 15:17:39 2024 +0100
@@ -676,7 +676,7 @@
         if (sym.startsWith("\\<longlonglong")) 4
         else if (sym.startsWith("\\<longlong")) 3
         else if (sym.startsWith("\\<long") || sym.startsWith("\\<Long")) 2
-        else if (is_printable(sym)) 1
+        else if (is_blank(sym) || is_printable(sym)) 1
         else 0
       }).sum
   }