--- a/src/Pure/General/long_name.ML Sat Apr 15 15:19:58 2023 +0200
+++ b/src/Pure/General/long_name.ML Sat Apr 15 22:26:22 2023 +0200
@@ -25,6 +25,7 @@
val count_chunks: chunks -> int
val size_chunks: chunks -> int
val empty_chunks: chunks
+ val base_chunks: string -> chunks
val make_chunks: int -> bool list -> string -> chunks
val chunks: string -> chunks
val explode_chunks: chunks -> string list
@@ -157,6 +158,9 @@
val chunks = make_chunks 0 [];
+fun base_chunks name =
+ make_chunks (Int.max (0, count name - 1)) [] name;
+
fun expand_chunks f (Chunks {count, size, mask, string}) =
let
val {string_end, chunk_end, ...} = string_ops string;