# HG changeset patch
# User wenzelm
# Date 1683020333 -7200
# Node ID fcd85e04a9489f880a4d9396b6446f9d52afdfe0
# Parent  27b5cb41c253567ff0c272118197d7c94102065f
minor performance tuning: no storage of accesses, produce Binding.full_name_spec on the spot;

diff -r 27b5cb41c253 -r fcd85e04a948 src/Pure/General/binding.ML
--- a/src/Pure/General/binding.ML	Tue May 02 11:11:19 2023 +0200
+++ b/src/Pure/General/binding.ML	Tue May 02 11:38:53 2023 +0200
@@ -45,6 +45,7 @@
   type name_spec =
     {restriction: bool option, concealed: bool, spec: (string * bool) list, full_name: string}
   val name_spec: scope list -> (string * bool) list -> binding -> name_spec
+  val full_name_spec: string -> name_spec
 end;
 
 structure Binding: BINDING =
@@ -220,6 +221,10 @@
     val full_name = Long_Name.implode (map #1 spec');
   in {restriction = restriction, concealed = concealed, spec = spec', full_name = full_name} end;
 
+fun full_name_spec name : name_spec =
+  let val spec = Long_Name.explode name |> map (rpair false);
+  in {restriction = NONE, concealed = false, spec = spec, full_name = name} end;
+
 end;
 
 type binding = Binding.binding;
diff -r 27b5cb41c253 -r fcd85e04a948 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Tue May 02 11:11:19 2023 +0200
+++ b/src/Pure/General/name_space.ML	Tue May 02 11:38:53 2023 +0200
@@ -143,11 +143,7 @@
 
 (* external accesses *)
 
-type external =
- {accesses: Long_Name.chunks list,
-  aliases: string list,
-  entry: entry};
-
+type external = {aliases: string list, entry: entry};
 type externals = external Change_Table.T;  (*name -> external*)
 
 
@@ -213,11 +209,6 @@
 fun lookup_internals (Name_Space {internals, ...}) = Long_Name.Chunks.lookup internals;
 fun lookup_externals (Name_Space {externals, ...}) = Change_Table.lookup externals;
 
-fun get_accesses space name =
-  (case lookup_externals space name of
-    NONE => []
-  | SOME {accesses, ...} => accesses);
-
 fun get_aliases space name =
   (case lookup_externals space name of
     NONE => [name]
@@ -389,22 +380,15 @@
         then raise Long_Name.Chunks.SAME
         else (Library.merge (op =) (names1, names2), Library.merge (op =) (names1', names2'))));
     val externals' = (externals1, externals2) |> Change_Table.join (fn name =>
-      fn ({accesses = accesses1, aliases = aliases1, entry = entry1},
-          {accesses = accesses2, aliases = aliases2, entry = entry2}) =>
-      if #serial entry1 <> #serial entry2
-      then err_dup kind' (name, entry1) (name, entry2) Position.none
-      else
-        let
-          val accesses' = Library.merge Long_Name.eq_chunks (accesses1, accesses2);
-          val aliases' = Library.merge (op =) (aliases1, aliases2);
-        in
-          if eq_list Long_Name.eq_chunks (accesses', accesses1) andalso
-             eq_list Long_Name.eq_chunks (accesses', accesses2) andalso
-             eq_list (op =) (aliases', aliases1) andalso
-             eq_list (op =) (aliases', aliases2)
-          then raise Change_Table.SAME
-          else {accesses = accesses', aliases = aliases', entry = entry1}
-        end);
+      fn ({aliases = aliases1, entry = entry1}, {aliases = aliases2, entry = entry2}) =>
+        if #serial entry1 <> #serial entry2
+        then err_dup kind' (name, entry1) (name, entry2) Position.none
+        else
+          let val aliases' = Library.merge (op =) (aliases1, aliases2) in
+            if eq_list (op =) (aliases', aliases1) andalso eq_list (op =) (aliases', aliases2)
+            then raise Change_Table.SAME
+            else {aliases = aliases', entry = entry1}
+          end);
   in make_name_space (kind', internals', externals') end;
 
 
@@ -525,7 +509,7 @@
   space |> map_name_space (fn (kind, internals, externals) =>
     let
       val _ = the_entry space name;
-      val accesses = get_accesses space name;
+      val accesses = get_aliases space name |> maps (make_accesses o Binding.full_name_spec);
       val accesses' = make_accesses' name;
       val xnames = filter (is_valid_access space name) accesses;
       val xnames' =
@@ -549,11 +533,8 @@
       val _ = alias_name = "" andalso error (Binding.bad binding);
 
       val internals' = internals |> fold (add_name name) more_accs;
-      val externals' = externals
-        |> Change_Table.map_entry name (fn {accesses, aliases, entry} =>
-            {accesses = fold_rev (update Long_Name.eq_chunks) more_accs accesses,
-             aliases = update (op =) alias_name aliases,
-             entry = entry});
+      val externals' = externals |> Change_Table.map_entry name
+        (fn {aliases, entry} => {aliases = update (op =) alias_name aliases, entry = entry});
     in (kind, internals', externals') end);
 
 
@@ -606,7 +587,7 @@
           val internals' = internals |> fold (add_name name) accesses;
           val externals' =
             (if strict then Change_Table.update_new else Change_Table.update)
-              (name, {accesses = accesses, aliases = [], entry = entry}) externals
+              (name, {aliases = [], entry = entry}) externals
             handle Change_Table.DUP dup =>
               err_dup kind (dup, #entry (the (lookup_externals space dup)))
                 (name, entry) (#pos entry);