added accesses';
authorwenzelm
Wed Jul 10 14:47:48 2002 +0200 (2002-07-10 ago)
changeset 13332f130bcf29620
parent 13331 47e9950a502d
child 13333 1f5745b76fb8
added accesses';
src/Pure/General/name_space.ML
     1.1 --- a/src/Pure/General/name_space.ML	Wed Jul 10 13:55:32 2002 +0200
     1.2 +++ b/src/Pure/General/name_space.ML	Wed Jul 10 14:47:48 2002 +0200
     1.3 @@ -21,6 +21,7 @@
     1.4    val map_base: (string -> string) -> string -> string
     1.5    val is_qualified: string -> bool
     1.6    val accesses: string -> string list
     1.7 +  val accesses': string -> string list
     1.8    type T
     1.9    val empty: T
    1.10    val extend: T * string list -> T
    1.11 @@ -64,6 +65,8 @@
    1.12      val pfxs = map (fn x => x @ [b]) (Library.prefixes1 q);
    1.13    in map pack (sfxs @ pfxs) end;
    1.14  
    1.15 +val accesses' = map pack o Library.suffixes1 o unpack;
    1.16 +
    1.17  
    1.18  
    1.19  (** name spaces **)
    1.20 @@ -142,7 +145,7 @@
    1.21        | try (nm :: nms) =
    1.22            let val (full_nm, uniq) = lookup space nm
    1.23            in if full_nm = name andalso uniq then nm else try nms end
    1.24 -  in try (map pack (Library.suffixes1 (unpack name))) end;
    1.25 +  in try (accesses' name) end;
    1.26  
    1.27  (*prune names on output by default*)
    1.28  val long_names = ref false;