more accurate Symbol.Metric, following 6eccae338770;

--- a/src/Pure/General/symbol.scala	Mon Nov 04 14:39:27 2024 +0100
+++ b/src/Pure/General/symbol.scala	Mon Nov 04 14:50:21 2024 +0100
@@ -673,7 +673,9 @@
     def apply(str: String): Double =
       (for (s <- iterator(str)) yield {
         val sym = encode(s)
-        if (sym.startsWith("\\<long") || sym.startsWith("\\<Long")) 2
+        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 0
       }).sum