src/Pure/General/name_space.ML
changeset 30277 4f2b6ccce047
parent 30242 aea5d7fa7ef5
child 30280 eb98b49ef835
     1.1 --- a/src/Pure/General/name_space.ML	Thu Mar 05 10:52:07 2009 +0100
     1.2 +++ b/src/Pure/General/name_space.ML	Thu Mar 05 10:53:49 2009 +0100
     1.3 @@ -123,7 +123,7 @@
     1.4  datatype T =
     1.5    NameSpace of
     1.6      (string list * string list) Symtab.table *   (*internals, hidden internals*)
     1.7 -    string list Symtab.table;                    (*externals*)
     1.8 +    xstring list Symtab.table;                   (*externals*)
     1.9  
    1.10  val empty = NameSpace (Symtab.empty, Symtab.empty);
    1.11  
    1.12 @@ -153,9 +153,9 @@
    1.13  
    1.14  fun extern_flags {long_names, short_names, unique_names} space name =
    1.15    let
    1.16 -    fun valid unique xname =
    1.17 -      let val (name', uniq) = lookup space xname
    1.18 -      in name = name' andalso (uniq orelse not unique) end;
    1.19 +    fun valid require_unique xname =
    1.20 +      let val (name', is_unique) = lookup space xname
    1.21 +      in name = name' andalso (not require_unique orelse is_unique) end;
    1.22  
    1.23      fun ext [] = if valid false name then name else hidden name
    1.24        | ext (nm :: nms) = if valid unique_names nm then nm else ext nms;
    1.25 @@ -278,8 +278,8 @@
    1.26  
    1.27  fun full_name naming binding =
    1.28    let
    1.29 -    val (prefix, qualifier, bname) = Binding.dest binding;
    1.30 -    val naming' = apply_prefix (prefix @ qualifier) naming;
    1.31 +    val (prfx, bname) = Binding.dest binding;
    1.32 +    val naming' = apply_prefix prfx naming;
    1.33    in full naming' bname end;
    1.34  
    1.35  
    1.36 @@ -287,8 +287,8 @@
    1.37  
    1.38  fun declare naming binding space =
    1.39    let
    1.40 -    val (prefix, qualifier, bname) = Binding.dest binding;
    1.41 -    val naming' = apply_prefix (prefix @ qualifier) naming;
    1.42 +    val (prfx, bname) = Binding.dest binding;
    1.43 +    val naming' = apply_prefix prfx naming;
    1.44      val name = full naming' bname;
    1.45      val names = explode_name name;
    1.46