# HG changeset patch
# User wenzelm
# Date 1729951651 -7200
# Node ID 6eccae3387706b101eab124edeed4aea0fc6785c
# Parent  a477ce2fe491bbfe03c75561f30c39fb199b4f58
more accurate Symbol.length;

diff -r a477ce2fe491 -r 6eccae338770 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Sat Oct 26 16:07:03 2024 +0200
+++ b/src/Pure/General/symbol.ML	Sat Oct 26 16:07:31 2024 +0200
@@ -501,7 +501,9 @@
 (* length *)
 
 fun sym_len s =
-  if String.isPrefix "\092<long" s orelse String.isPrefix "\092<Long" s then 2
+  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 0;