minor performance tuning: more compact, more sharing;

--- a/src/Pure/General/long_name.ML	Mon May 01 12:18:10 2023 +0200
+++ b/src/Pure/General/long_name.ML	Mon May 01 13:09:53 2023 +0200
@@ -25,6 +25,7 @@
   val count_chunks: chunks -> int
   val size_chunks: chunks -> int
   val empty_chunks: chunks
+  val is_empty_chunks: chunks -> bool
   val base_chunks: string -> chunks
   val suppress_chunks: int -> bool list -> string -> chunks
   val make_chunks: string -> chunks
@@ -107,18 +108,26 @@
 fun range_length r = r mod range_limit;
 fun range_string s r = String.substring (s, range_index r, range_length r);
 
+val range_empty = 0;
+val ranges_empty: int vector = Vector.fromList [];
+
 in
 
-abstype chunks = Chunks of {ranges: int vector (*reverse*), string: string}
+abstype chunks = Chunks of {range0: int, ranges: int vector (*reverse*), string: string}
 with
 
-fun count_chunks (Chunks {ranges, ...}) = Vector.length ranges;
+val empty_chunks = Chunks {range0 = range_empty, ranges = ranges_empty, string = ""};
+
+fun is_empty_chunks (Chunks {range0, ranges, ...}) =
+  range0 = range_empty andalso Vector.length ranges = 0;
 
-fun size_chunks (Chunks {ranges, ...}) =
-  if Vector.length ranges = 0 then 0
-  else Vector.fold (fn r => fn n => n + range_length r + 1) ranges ~1;
+fun count_chunks (chunks as Chunks {ranges, ...}) =
+  if is_empty_chunks chunks then 0
+  else Vector.length ranges + 1;
 
-val empty_chunks = Chunks {ranges = Vector.fromList [], string = ""};
+fun size_chunks (chunks as Chunks {range0, ranges, ...}) =
+  if is_empty_chunks chunks then 0
+  else Vector.fold (fn r => fn n => n + range_length r + 1) ranges (range_length range0);
 
 fun base_chunks name =
   let
@@ -126,7 +135,7 @@
     val j = i + 1;
   in
     if i < 0 then empty_chunks
-    else Chunks {ranges = Vector.fromList [range name j (size name - j)], string = name}
+    else Chunks {range0 = range name j (size name - j), ranges = ranges_empty, string = name}
   end;
 
 fun suppress_chunks suppress1 suppress2 string =
@@ -158,25 +167,30 @@
         if not string_end then suppr_chunks suppr1' suppr2' i' j' rs'
         else if not (suppr1' = 0 andalso null suppr2') then
           failure string ("cannot suppress chunks beyond " ^ string_of_int (length rs'))
-        else if null rs' then empty_chunks
-        else Chunks {ranges = Vector.fromList rs', string = string}
+        else
+          (case rs' of
+            [] => empty_chunks
+          | r0 :: rest => Chunks {range0 = r0, ranges = Vector.fromList rest, string = string})
       end;
   in suppr_chunks suppress1 suppress2 0 0 [] end;
 
 val make_chunks = suppress_chunks 0 [];
 
-fun explode_chunks (Chunks {ranges, string}) =
-  Vector.fold (cons o range_string string) ranges [];
+fun explode_chunks (chunks as Chunks {range0, ranges, string}) =
+  if is_empty_chunks chunks then []
+  else Vector.fold (cons o range_string string) ranges [range_string string range0];
 
-fun implode_chunks (chunks as Chunks {ranges, string}) =
+fun implode_chunks (chunks as Chunks {range0, ranges, string}) =
   if size_chunks chunks = size string then string
-  else if Vector.length ranges = 1 then range_string string (Vector.nth ranges 0)
+  else if Vector.length ranges = 0 then range_string string range0
   else implode (explode_chunks chunks);
 
 val compare_chunks = pointer_eq_ord (fn (chunks1, chunks2) =>
   let
-    val Chunks {ranges = ranges1, string = string1} = chunks1;
-    val Chunks {ranges = ranges2, string = string2} = chunks2;
+    val Chunks {range0 = range01, ranges = ranges1, string = string1} = chunks1;
+    val Chunks {range0 = range02, ranges = ranges2, string = string2} = chunks2;
+    val count1 = count_chunks chunks1;
+    val count2 = count_chunks chunks2;
 
     val range_length_ord = int_ord o apply2 range_length;
     fun range_substring_ord arg =
@@ -192,9 +206,20 @@
           else EQUAL;
       in (case int_ord (m, n) of EQUAL => substring_ord 0 | ord => ord) end;
   in
-    (case vector_ord range_length_ord (ranges1, ranges2) of
-      EQUAL => Vector.collate range_substring_ord (ranges1, ranges2)
-    | ord => ord)
+    if count1 = 0 andalso count2 = 0 then EQUAL
+    else
+      (case int_ord (count1, count2) of
+        EQUAL =>
+          (case range_length_ord (range01, range02) of
+            EQUAL =>
+              (case Vector.collate range_length_ord (ranges1, ranges2) of
+                EQUAL =>
+                  (case range_substring_ord (range01, range02) of
+                    EQUAL => Vector.collate range_substring_ord (ranges1, ranges2)
+                  | ord => ord)
+              | ord => ord)
+          | ord => ord)
+      | ord => ord)
   end);
 
 val eq_chunks = is_equal o compare_chunks;