compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology);

--- a/src/Pure/General/long_name.ML	Thu Apr 13 23:08:39 2023 +0200
+++ b/src/Pure/General/long_name.ML	Thu Apr 13 23:16:18 2023 +0200
@@ -21,12 +21,26 @@
   val qualifier: string -> string
   val base_name: string -> string
   val map_base_name: (string -> string) -> string -> string
+  type chunks
+  val count_chunks: chunks -> int
+  val size_chunks: chunks -> int
+  val empty_chunks: chunks
+  val make_chunks: bool list -> string -> chunks
+  val chunks: string -> chunks
+  val explode_chunks: chunks -> string list
+  val implode_chunks: chunks -> string
+  val compare_chunks: chunks * chunks -> order
+  val eq_chunks: chunks * chunks -> bool
+  structure Chunks: CHANGE_TABLE
 end;
 
 structure Long_Name: LONG_NAME =
 struct
 
+(* long names separated by "." *)
+
 val separator = ".";
+val separator_char = String.sub (separator, 0);
 
 val is_qualified = exists_string (fn s => s = separator);
 
@@ -63,4 +77,112 @@
       let val names = explode name
       in implode (nth_map (length names - 1) f names) end;
 
+
+(* compact representation of chunks *)
+
+local
+
+fun mask_bad s = s = 0w0;
+fun mask_set s m = Word.orb (m, s);
+fun mask_push s = Word.<< (s, 0w1);
+fun mask_next m = Word.>> (m, 0w1);
+fun mask_keep m = Word.andb (m, 0w1) = 0w0;
+
+fun string_ops string =
+  let
+    val n = size string;
+    fun char i = String.sub (string, i);
+    fun string_end i = i >= n;
+    fun chunk_end i = string_end i orelse char i = separator_char;
+  in {string_end = string_end, chunk_end = chunk_end} end;
+
+in
+
+abstype chunks = Chunks of {count: int, size: int, mask: word, string: string}
+with
+
+fun count_chunks (Chunks {count, ...}) = count;
+fun size_chunks (Chunks {size, ...}) = size;
+
+val empty_chunks = Chunks {count = 0, size = 0, mask = 0w0, string = ""};
+
+fun make_chunks suppress string =
+  let
+    val {string_end, chunk_end, ...} = string_ops string;
+
+    fun err msg = raise Fail ("Malformed qualified name " ^ quote string ^ ":\n  " ^ msg);
+
+    fun make suppr i k l m s =
+      let
+        val is_end = chunk_end i;
+        val keep = null suppr orelse not (hd suppr);
+
+        val suppr' = if is_end andalso not (null suppr) then tl suppr else suppr;
+        val l' = if keep then l + 1 else l;
+        val k' = if is_end andalso keep andalso l' > 0 then k + 1 else k;
+        val m' =
+          if not is_end orelse keep then m
+          else if mask_bad s then
+            err ("cannot suppress chunks beyond word size " ^ string_of_int Word.wordSize)
+          else mask_set s m;
+        val s' = if is_end then mask_push s else s;
+      in
+        if not (string_end i) then make suppr' (i + 1) k' l' m' s'
+        else if not (null suppr') then err ("cannot suppress chunks beyond " ^ string_of_int k')
+        else if k' = 0 then empty_chunks
+        else Chunks {count = k', size = Int.max (0, l' - 1), mask = m', string = string}
+      end;
+  in make suppress 0 0 0 0w0 0w1 end;
+
+val chunks = make_chunks [];
+
+fun expand_chunks f (Chunks {count, size, mask, string}) =
+  let
+    val {string_end, chunk_end, ...} = string_ops string;
+
+    fun explode bg en m acc =
+      let
+        val is_end = chunk_end en;
+
+        val en' = en + 1;
+        val bg' = if is_end then en' else bg;
+        val m' = if is_end then mask_next m else m;
+        val acc' = if is_end andalso mask_keep m then f (string, bg, en - bg) :: acc else acc;
+      in if string_end en then rev acc' else explode bg' en' m' acc' end;
+  in
+    if count = 0 then []
+    else if count = 1 andalso size = String.size string then [f (string, 0, size)]
+    else explode 0 0 mask []
+  end;
+
+val explode_chunks = expand_chunks String.substring;
+val implode_chunks = implode o explode_chunks;
+
+val compare_chunks =
+  pointer_eq_ord (fn (chunks1, chunks2) =>
+    let
+      val Chunks args1 = chunks1;
+      val Chunks args2 = chunks2;
+      val ord1 =
+        int_ord o apply2 #size |||
+        int_ord o apply2 #count;
+      val ord2 =
+        dict_ord int_ord o apply2 (expand_chunks #3) |||
+        dict_ord Substring.compare o apply2 (expand_chunks Substring.substring);
+    in
+      (case ord1 (args1, args2) of
+        EQUAL =>
+          if #mask args1 = #mask args2 andalso #string args1 = #string args2 then EQUAL
+          else ord2 (chunks1, chunks2)
+      | ord => ord)
+    end);
+
+val eq_chunks = is_equal o compare_chunks;
+
 end;
+
+end;
+
+structure Chunks = Change_Table(type key = chunks val ord = compare_chunks);
+
+end;

--- a/src/Pure/ML/ml_syntax.ML	Thu Apr 13 23:08:39 2023 +0200
+++ b/src/Pure/ML/ml_syntax.ML	Thu Apr 13 23:16:18 2023 +0200
@@ -139,8 +139,14 @@
       else take (Int.max (max_len, 0)) body @ ["..."];
   in Pretty.str (quote (implode (map print_symbol body'))) end;
 
+fun pretty_string' depth = pretty_string (FixedInt.toInt (depth * 100));
+
 val _ =
   ML_system_pp (fn depth => fn _ => fn str =>
-    Pretty.to_polyml (pretty_string (FixedInt.toInt (depth * 100)) str));
+    Pretty.to_polyml (pretty_string' depth str));
+
+val _ =
+  ML_system_pp (fn depth => fn _ => fn chunks =>
+    Pretty.to_polyml (pretty_string' depth (Long_Name.implode_chunks chunks)));
 
 end;

--- a/src/Pure/ROOT.ML	Thu Apr 13 23:08:39 2023 +0200
+++ b/src/Pure/ROOT.ML	Thu Apr 13 23:16:18 2023 +0200
@@ -72,6 +72,7 @@
 ML_file "General/ord_list.ML";
 ML_file "General/balanced_tree.ML";
 ML_file "General/linear_set.ML";
+ML_file "General/change_table.ML";
 ML_file "General/buffer.ML";
 ML_file "General/pretty.ML";
 ML_file "General/rat.ML";
@@ -96,7 +97,6 @@
 ML_file "PIDE/document_id.ML";
 ML_file "General/socket_io.ML";
 
-ML_file "General/change_table.ML";
 ML_file "General/graph.ML";
 
 ML_file "System/options.ML";