# HG changeset patch
# User wenzelm
# Date 1730728221 -3600
# Node ID e181259e539b99c6bca1d4fa1be436a64333e3ab
# Parent  545d474ada44271ca9e12ff18b3c431a7e61a2e1
more accurate Symbol.Metric, following 6eccae338770;

diff -r 545d474ada44 -r e181259e539b src/Pure/General/symbol.scala
--- 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