src/Pure/General/symbol.scala
changeset 81375 ae5695161423
parent 81339 e181259e539b
child 81429 0ccfc82fff57
--- 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
   }