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 }