# HG changeset patch
# User wenzelm
# Date 1681459950 -7200
# Node ID 5b798c255af13b383d42c20f02a58269b55c5ac9
# Parent  52e753197496da78f603bdd7fafe1c56d93462e6# Parent  f56697bfd67b2e487e840afe4c386b7d15a3f300
merged

diff -r 52e753197496 -r 5b798c255af1 src/Pure/General/binding.ML
--- a/src/Pure/General/binding.ML	Thu Apr 13 14:54:03 2023 +0200
+++ b/src/Pure/General/binding.ML	Fri Apr 14 10:12:30 2023 +0200
@@ -43,7 +43,7 @@
   val bad: binding -> string
   val check: binding -> unit
   val name_spec: scope list -> (string * bool) list -> binding ->
-    {restriction: bool option, concealed: bool, spec: (string * bool) list}
+    {restriction: bool option, concealed: bool, spec: (string * bool) list, full_name: string}
 end;
 
 structure Binding: BINDING =
@@ -211,8 +211,10 @@
     val _ =
       exists (fn (a, _) => member (op =) bad_specs a orelse exists_string (fn s => s = "\"") a) spec
       andalso error (bad binding);
-  in {restriction = restriction, concealed = concealed, spec = if null spec2 then [] else spec} end;
 
+    val spec' = if null spec2 then [] else spec;
+    val full_name = Long_Name.implode (map #1 spec');
+  in {restriction = restriction, concealed = concealed, spec = spec', full_name = full_name} end;
 
 end;
 
diff -r 52e753197496 -r 5b798c255af1 src/Pure/General/long_name.ML
--- a/src/Pure/General/long_name.ML	Thu Apr 13 14:54:03 2023 +0200
+++ b/src/Pure/General/long_name.ML	Fri Apr 14 10:12:30 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);
 
@@ -52,15 +66,130 @@
   if qual = "" orelse name = "" then name
   else qual ^ separator ^ name;
 
-fun qualifier "" = ""
-  | qualifier name = implode (#1 (split_last (explode name)));
-
-fun base_name "" = ""
-  | base_name name = List.last (explode name);
-
 fun map_base_name _ "" = ""
   | map_base_name f name =
       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);
+
+
+(* split name *)
+
+fun qualifier name =
+  if is_qualified name
+  then String.substring (name, 0, Int.max (0, List.last (expand_chunks #2 (chunks name)) - 1))
+  else "";
+
+fun base_name name =
+  if is_qualified name
+  then String.substring (List.last (expand_chunks I (chunks name)))
+  else name;
+
+end;
diff -r 52e753197496 -r 5b798c255af1 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Thu Apr 13 14:54:03 2023 +0200
+++ b/src/Pure/General/name_space.ML	Fri Apr 14 10:12:30 2023 +0200
@@ -126,7 +126,8 @@
 
 (* internal names *)
 
-type internals = (string list * string list) Change_Table.T;  (*xname -> visible, hidden*)
+type internal = string list * string list;  (*visible, hidden*)
+type internals = internal Change_Table.T;  (*xname -> internal*)
 
 fun map_internals f xname : internals -> internals =
   Change_Table.map_default (xname, ([], [])) f;
@@ -140,57 +141,59 @@
 
 (* external accesses *)
 
-type accesses = (xstring list * xstring list);  (*input / output fragments*)
-type entries = (accesses * entry) Change_Table.T;  (*name -> accesses, entry*)
+type external = {accesses: xstring list, accesses': xstring list, entry: entry};
+type externals = external Change_Table.T;  (*name -> external*)
 
 
 (* datatype T *)
 
-datatype T = Name_Space of {kind: string, internals: internals, entries: entries};
+datatype T = Name_Space of {kind: string, internals: internals, externals: externals};
 
-fun make_name_space (kind, internals, entries) =
-  Name_Space {kind = kind, internals = internals, entries = entries};
+fun make_name_space (kind, internals, externals) =
+  Name_Space {kind = kind, internals = internals, externals = externals};
 
-fun map_name_space f (Name_Space {kind = kind, internals = internals, entries = entries}) =
-  make_name_space (f (kind, internals, entries));
+fun map_name_space f (Name_Space {kind = kind, internals = internals, externals = externals}) =
+  make_name_space (f (kind, internals, externals));
 
-fun change_base_space begin = map_name_space (fn (kind, internals, entries) =>
-  (kind, Change_Table.change_base begin internals, Change_Table.change_base begin entries));
+fun change_base_space begin = map_name_space (fn (kind, internals, externals) =>
+  (kind, Change_Table.change_base begin internals, Change_Table.change_base begin externals));
 
-val change_ignore_space = map_name_space (fn (kind, internals, entries) =>
-  (kind, Change_Table.change_ignore internals, Change_Table.change_ignore entries));
+val change_ignore_space = map_name_space (fn (kind, internals, externals) =>
+  (kind, Change_Table.change_ignore internals, Change_Table.change_ignore externals));
 
 
 fun empty kind = make_name_space (kind, Change_Table.empty, Change_Table.empty);
 
 fun kind_of (Name_Space {kind, ...}) = kind;
+fun lookup_internals (Name_Space {internals, ...}) = Change_Table.lookup internals;
+fun lookup_externals (Name_Space {externals, ...}) = Change_Table.lookup externals;
 
-fun gen_markup def (Name_Space {kind, entries, ...}) name =
-  (case Change_Table.lookup entries name of
+fun gen_markup def space name =
+  (case lookup_externals space name of
     NONE => Markup.intensify
-  | SOME (_, entry) => entry_markup def kind (name, entry));
+  | SOME {entry, ...} => entry_markup def (kind_of space) (name, entry));
 
 val markup = gen_markup {def = false};
 val markup_def = gen_markup {def = true};
 
-fun undefined (space as Name_Space {kind, entries, ...}) bad =
+fun undefined (space as Name_Space {kind, externals, ...}) bad =
   let
     val (prfx, sfx) =
       (case Long_Name.dest_hidden bad of
         SOME name =>
-          if Change_Table.defined entries name
+          if Change_Table.defined externals name
           then ("Inaccessible", Markup.markup (markup space name) (quote name))
           else ("Undefined", quote name)
       | NONE => ("Undefined", quote bad));
   in prfx ^ " " ^ plain_words kind ^ ": " ^ sfx end;
 
-fun get_names (Name_Space {entries, ...}) =
-  Change_Table.fold (cons o #1) entries [];
+fun get_names (Name_Space {externals, ...}) =
+  Change_Table.fold (cons o #1) externals [];
 
-fun the_entry (space as Name_Space {entries, ...}) name =
-  (case Change_Table.lookup entries name of
+fun the_entry space name =
+  (case lookup_externals space name of
     NONE => error (undefined space name)
-  | SOME (_, entry) => entry);
+  | SOME {entry, ...} => entry);
 
 fun the_entry_theory_name space name =
   Long_Name.base_name (#theory_long_name (the_entry space name));
@@ -203,8 +206,8 @@
 
 (* intern *)
 
-fun intern' (Name_Space {internals, ...}) xname =
-  (case the_default ([], []) (Change_Table.lookup internals xname) of
+fun intern' space xname =
+  (case the_default ([], []) (lookup_internals space xname) of
     ([name], _) => (name, true)
   | (name :: _, _) => (name, false)
   | ([], []) => (Long_Name.hidden xname, true)
@@ -212,13 +215,8 @@
 
 val intern = #1 oo intern';
 
-fun get_accesses (Name_Space {entries, ...}) name =
-  (case Change_Table.lookup entries name of
-    NONE => ([], [])
-  | SOME (accesses, _) => accesses);
-
-fun is_valid_access (Name_Space {internals, ...}) name xname =
-  (case Change_Table.lookup internals xname of
+fun is_valid_access space name xname =
+  (case lookup_internals space xname of
     SOME (name' :: _, _) => name = name'
   | _ => false);
 
@@ -239,12 +237,15 @@
       let val (name', is_unique) = intern' space xname
       in name = name' andalso (not require_unique orelse is_unique) end;
 
-    fun ext [] = if valid false name then name else Long_Name.hidden name
-      | ext (nm :: nms) = if valid names_unique nm then nm else ext nms;
+    fun extern [] = if valid false name then name else Long_Name.hidden name
+      | extern (a :: bs) = if valid names_unique a then a else extern bs;
   in
     if names_long then name
     else if names_short then Long_Name.base_name name
-    else ext (#2 (get_accesses space name))
+    else
+      (case lookup_externals space name of
+        NONE => extern []
+      | SOME {accesses', ...} => extern accesses')
   end;
 
 fun extern_ord ctxt space = string_ord o apply2 (extern ctxt space);
@@ -301,8 +302,8 @@
 (* merge *)
 
 fun merge
-  (Name_Space {kind = kind1, internals = internals1, entries = entries1},
-    Name_Space {kind = kind2, internals = internals2, entries = entries2}) =
+  (Name_Space {kind = kind1, internals = internals1, externals = externals1},
+    Name_Space {kind = kind2, internals = internals2, externals = externals2}) =
   let
     val kind' =
       if kind1 = kind2 then kind1
@@ -313,11 +314,11 @@
         if pointer_eq (names1, names2) andalso pointer_eq (names1', names2')
         then raise Change_Table.SAME
         else (Library.merge (op =) (names1, names2), Library.merge (op =) (names1', names2'))));
-    val entries' = (entries1, entries2) |> Change_Table.join
-      (fn name => fn ((_, entry1), (_, entry2)) =>
+    val externals' = (externals1, externals2) |> Change_Table.join
+      (fn name => fn ({entry = entry1, ...}, {entry = entry2, ...}) =>
         if #serial entry1 = #serial entry2 then raise Change_Table.SAME
         else err_dup kind' (name, entry1) (name, entry2) Position.none);
-  in make_name_space (kind', internals', entries') end;
+  in make_name_space (kind', internals', externals') end;
 
 
 
@@ -427,15 +428,15 @@
 fun name_spec naming binding =
   Binding.name_spec (get_scopes naming) (get_path naming) (transform_binding naming binding);
 
-fun full_name naming =
-  name_spec naming #> #spec #> map #1 #> Long_Name.implode;
-
-val base_name = full_name global_naming #> Long_Name.base_name;
+val full_name = #full_name oo name_spec;
+val base_name = Long_Name.base_name o full_name global_naming;
 
 
 (* accesses *)
 
-fun mandatory xs = map_filter (fn (x, true) => SOME x | _ => NONE) xs;
+local
+
+fun mandatory xs = fold_rev (fn (x, b) => b ? cons x) xs [];
 
 fun mandatory_prefixes xs = mandatory xs :: mandatory_prefixes1 xs
 and mandatory_prefixes1 [] = []
@@ -444,46 +445,57 @@
 
 fun mandatory_suffixes xs = map rev (mandatory_prefixes (rev xs));
 
+in
+
 fun make_accesses naming binding =
-  (case name_spec naming binding of
-    {restriction = SOME true, ...} => ([], [])
-  | {restriction, spec, ...} =>
-      let
-        val restrict = is_some restriction ? filter (fn [_] => false | _ => true);
-        val sfxs = restrict (mandatory_suffixes spec);
-        val pfxs = restrict (mandatory_prefixes spec);
-      in apply2 (map Long_Name.implode) (sfxs @ pfxs, sfxs) end);
+  let
+    val args as {restriction, spec, ...} = name_spec naming binding;
+    val accesses =
+      if restriction = SOME true then ([], [])
+      else
+        let
+          val restrict = is_some restriction ? filter (fn [_] => false | _ => true);
+          val sfxs = restrict (mandatory_suffixes spec);
+          val pfxs = restrict (mandatory_prefixes spec);
+        in apply2 (map Long_Name.implode o distinct op =) (sfxs @ pfxs, sfxs) end;
+  in (accesses, args) end;
+
+end;
 
 
 (* hide *)
 
 fun hide fully name space =
-  space |> map_name_space (fn (kind, internals, entries) =>
+  space |> map_name_space (fn (kind, internals, externals) =>
     let
       val _ = the_entry space name;
-      val (accs, accs') = get_accesses space name;
-      val xnames = filter (is_valid_access space name) accs;
+      val (accesses, accesses') =
+        (case lookup_externals space name of
+          NONE => ([], [])
+        | SOME {accesses, accesses', ...} => (accesses, accesses'));
+      val xnames = filter (is_valid_access space name) accesses;
       val internals' = internals
         |> hide_name name
         |> fold (del_name name)
           (if fully then xnames else inter (op =) [Long_Name.base_name name] xnames)
-        |> fold (del_name_extra name) accs';
-    in (kind, internals', entries) end);
+        |> fold (del_name_extra name) accesses';
+    in (kind, internals', externals) end);
 
 
 (* alias *)
 
 fun alias naming binding name space =
-  space |> map_name_space (fn (kind, internals, entries) =>
+  space |> map_name_space (fn (kind, internals, externals) =>
     let
       val _ = the_entry space name;
-      val (more_accs, more_accs') = make_accesses naming binding;
+      val (more_accs, more_accs') = #1 (make_accesses naming binding);
       val internals' = internals |> fold (add_name name) more_accs;
-      val entries' = entries
-        |> Change_Table.map_entry name (apfst (fn (accs, accs') =>
-            (fold_rev (update op =) more_accs accs,
-             fold_rev (update op =) more_accs' accs')))
-    in (kind, internals', entries') end);
+      val externals' = externals
+        |> Change_Table.map_entry name (fn {accesses, accesses', entry} =>
+            {accesses = fold_rev (update op =) more_accs accesses,
+             accesses' = fold_rev (update op =) more_accs' accesses',
+             entry = entry});
+    in (kind, internals', externals') end);
 
 
 
@@ -512,16 +524,13 @@
 
 (* declaration *)
 
-fun declared (Name_Space {entries, ...}) = Change_Table.defined entries;
+fun declared (Name_Space {externals, ...}) = Change_Table.defined externals;
 
 fun declare context strict binding space =
   let
     val naming = naming_of context;
     val Naming {group, theory_long_name, ...} = naming;
-    val {concealed, spec, ...} = name_spec naming binding;
-    val accesses = make_accesses naming binding;
-
-    val name = Long_Name.implode (map fst spec);
+    val ((accesses, accesses'), {concealed, full_name = name, ...}) = make_accesses naming binding;
     val _ = name = "" andalso error (Binding.bad binding);
 
     val (proper_pos, pos) = Position.default (Binding.pos_of binding);
@@ -532,16 +541,16 @@
       pos = pos,
       serial = serial ()};
     val space' =
-      space |> map_name_space (fn (kind, internals, entries) =>
+      space |> map_name_space (fn (kind, internals, externals) =>
         let
-          val internals' = internals |> fold (add_name name) (#1 accesses);
-          val entries' =
+          val internals' = internals |> fold (add_name name) accesses;
+          val externals' =
             (if strict then Change_Table.update_new else Change_Table.update)
-              (name, (accesses, entry)) entries
+              (name, {accesses = accesses, accesses' = accesses', entry = entry}) externals
             handle Change_Table.DUP dup =>
-              err_dup kind (dup, #2 (the (Change_Table.lookup entries dup)))
+              err_dup kind (dup, #entry (the (lookup_externals space dup)))
                 (name, entry) (#pos entry);
-        in (kind, internals', entries') end);
+        in (kind, internals', externals') end);
     val _ =
       if proper_pos andalso Context_Position.is_reported_generic context pos then
         Position.report pos (entry_markup {def = true} (kind_of space) (name, entry))
diff -r 52e753197496 -r 5b798c255af1 src/Pure/General/set.ML
--- a/src/Pure/General/set.ML	Thu Apr 13 14:54:03 2023 +0200
+++ b/src/Pure/General/set.ML	Fri Apr 14 10:12:30 2023 +0200
@@ -23,6 +23,7 @@
   val get_first: (elem -> 'a option) -> T -> 'a option
   val member: T -> elem -> bool
   val subset: T * T -> bool
+  val eq_set: T * T -> bool
   val ord: T ord
   val insert: elem -> T -> T
   val make: elem list -> T
@@ -278,6 +279,9 @@
 
 fun subset (set1, set2) = forall (member set2) set1;
 
+fun eq_set (set1, set2) =
+  pointer_eq (set1, set2) orelse size set1 = size set2 andalso subset (set1, set2);
+
 val ord =
   pointer_eq_ord (fn sets =>
     (case int_ord (apply2 size sets) of
diff -r 52e753197496 -r 5b798c255af1 src/Pure/ML/ml_syntax.ML
--- a/src/Pure/ML/ml_syntax.ML	Thu Apr 13 14:54:03 2023 +0200
+++ b/src/Pure/ML/ml_syntax.ML	Fri Apr 14 10:12:30 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;
diff -r 52e753197496 -r 5b798c255af1 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Thu Apr 13 14:54:03 2023 +0200
+++ b/src/Pure/ROOT.ML	Fri Apr 14 10:12:30 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";
diff -r 52e753197496 -r 5b798c255af1 src/Pure/term_items.ML
--- a/src/Pure/term_items.ML	Thu Apr 13 14:54:03 2023 +0200
+++ b/src/Pure/term_items.ML	Fri Apr 14 10:12:30 2023 +0200
@@ -78,7 +78,7 @@
 fun make_set xs = build (fold add_set xs);
 
 fun subset (A: set, B: set) = forall (defined B o #1) A;
-fun eq_set (A: set, B: set) = size A = size B andalso subset (A, B);
+fun eq_set (A: set, B: set) = pointer_eq (A, B) orelse size A = size B andalso subset (A, B);
 
 fun list_set_ord ord (Table tab) = tab |> Table.dest |> sort (ord o apply2 #2) |> map #1;
 val list_set = list_set_ord int_ord;