# HG changeset patch
# User wenzelm
# Date 1683320230 -7200
# Node ID b256ac9c0577c6263aeeb5d6a70157479eb3eb0f
# Parent  31ea5c1f874d18cf7cee277b08faa98d5bd65539
more complete accesses for "extern" operation, notably for aliases;

diff -r 31ea5c1f874d -r b256ac9c0577 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Fri May 05 15:56:12 2023 +0200
+++ b/src/Pure/General/name_space.ML	Fri May 05 22:57:10 2023 +0200
@@ -239,7 +239,7 @@
     SOME (name' :: _, _) => name = name'
   | _ => false);
 
-fun get_accesses {intern, aliases} space name =
+fun get_accesses {intern, aliases, valid} space name =
   let
     fun accesses a =
       let
@@ -249,7 +249,7 @@
           | NONE => [])
       in
         make_accesses {intern = intern} NONE suppress a
-        |> filter (is_valid_access space a)
+        |> valid ? filter (is_valid_access space a)
       end;
   in if aliases then maps accesses (get_aliases space name) else accesses name end;
 
@@ -322,7 +322,7 @@
 
     fun extern_name name =
       get_first (extern_chunks names_unique name)
-        (get_accesses {intern = false, aliases = false} space name);
+        (get_accesses {intern = false, aliases = false, valid = false} space name);
 
     fun extern_names aliases =
       (case get_first extern_name aliases of
@@ -530,9 +530,9 @@
     let
       val _ = the_entry space name;
       val accesses =
-        get_accesses {intern = true, aliases = true} space name
+        get_accesses {intern = true, aliases = true, valid = true} space name
         |> not fully ? inter Long_Name.eq_chunks [Long_Name.base_chunks name];
-      val accesses' = get_accesses {intern = false, aliases = false} space name;
+      val accesses' = get_accesses {intern = false, aliases = false, valid = true} space name;
       val internals' = internals
         |> hide_name name
         |> fold (del_name name) accesses