src/Pure/General/name_space.ML
changeset 30222 4102bbf2af21
parent 30215 47cce3d47e62
child 30233 6eb726e43ed1
     1.1 --- a/src/Pure/General/name_space.ML	Tue Mar 03 17:42:30 2009 +0100
     1.2 +++ b/src/Pure/General/name_space.ML	Tue Mar 03 18:31:59 2009 +0100
     1.3 @@ -6,7 +6,6 @@
     1.4  Cf. Pure/General/binding.ML
     1.5  *)
     1.6  
     1.7 -type bstring = string;    (*simple names to be bound -- legacy*)
     1.8  type xstring = string;    (*external names*)
     1.9  
    1.10  signature BASIC_NAME_SPACE =
    1.11 @@ -67,8 +66,8 @@
    1.12  fun hidden name = "??." ^ name;
    1.13  val is_hidden = String.isPrefix "??.";
    1.14  
    1.15 -val separator = Binding.separator;
    1.16 -val is_qualified = Binding.is_qualified;
    1.17 +val separator = ".";
    1.18 +val is_qualified = exists_string (fn s => s = separator);
    1.19  
    1.20  val implode_name = space_implode separator;
    1.21  val explode_name = space_explode separator;
    1.22 @@ -295,13 +294,13 @@
    1.23      in space |> fold (add_name name) accs |> put_accesses name accs' end;
    1.24  
    1.25  fun full_name naming b =
    1.26 -  let val (prefix, bname) = Binding.dest b
    1.27 -  in full_internal (apply_prefix prefix naming) bname end;
    1.28 +  let val (prefix, qualifier, bname) = Binding.dest b
    1.29 +  in full_internal (apply_prefix (prefix @ qualifier) naming) bname end;
    1.30  
    1.31  fun declare bnaming b =
    1.32    let
    1.33 -    val (prefix, bname) = Binding.dest b;
    1.34 -    val naming = apply_prefix prefix bnaming;
    1.35 +    val (prefix, qualifier, bname) = Binding.dest b;
    1.36 +    val naming = apply_prefix (prefix @ qualifier) bnaming;
    1.37      val name = full_internal naming bname;
    1.38    in declare_internal naming name #> pair name end;
    1.39