src/Pure/General/name_space.ML
changeset 21858 05f57309170c
parent 20530 448594cbd82b
child 21914 77372f38aa98
     1.1 --- a/src/Pure/General/name_space.ML	Thu Dec 14 22:19:39 2006 +0100
     1.2 +++ b/src/Pure/General/name_space.ML	Fri Dec 15 00:08:06 2006 +0100
     1.3 @@ -22,8 +22,8 @@
     1.4    val hidden: string -> string
     1.5    val separator: string                 (*single char*)
     1.6    val is_qualified: string -> bool
     1.7 -  val pack: string list -> string
     1.8 -  val unpack: string -> string list
     1.9 +  val implode: string list -> string
    1.10 +  val explode: string -> string list
    1.11    val append: string -> string -> string
    1.12    val qualified: string -> string -> string
    1.13    val base: string -> string
    1.14 @@ -70,8 +70,8 @@
    1.15  val separator = ".";
    1.16  val is_qualified = exists_string (fn s => s = separator);
    1.17  
    1.18 -val pack = space_implode separator;
    1.19 -val unpack = space_explode separator;
    1.20 +val implode_name = space_implode separator;
    1.21 +val explode_name = space_explode separator;
    1.22  
    1.23  fun append name1 "" = name1
    1.24    | append "" name2 = name2
    1.25 @@ -82,15 +82,15 @@
    1.26    else path ^ separator ^ name;
    1.27  
    1.28  fun base "" = ""
    1.29 -  | base name = List.last (unpack name);
    1.30 +  | base name = List.last (explode_name name);
    1.31  
    1.32  fun qualifier "" = ""
    1.33 -  | qualifier name = pack (#1 (split_last (unpack name)));
    1.34 +  | qualifier name = implode_name (#1 (split_last (explode_name name)));
    1.35  
    1.36  fun map_base _ "" = ""
    1.37    | map_base f name =
    1.38 -      let val names = unpack name
    1.39 -      in pack (nth_map (length names - 1) f names) end;
    1.40 +      let val names = explode_name name
    1.41 +      in implode_name (nth_map (length names - 1) f names) end;
    1.42  
    1.43  
    1.44  (* accesses *)
    1.45 @@ -117,8 +117,8 @@
    1.46        [xs @ ys] @@ prefixes1 zs @@ [ws];
    1.47    in sfxs @ pfxs end;
    1.48  
    1.49 -val accesses = map pack o suffixes_prefixes o unpack;
    1.50 -val accesses' = map pack o Library.suffixes1 o unpack;
    1.51 +val accesses = map implode_name o suffixes_prefixes o explode_name;
    1.52 +val accesses' = map implode_name o Library.suffixes1 o explode_name;
    1.53  
    1.54  
    1.55  
    1.56 @@ -228,10 +228,10 @@
    1.57    if is_hidden name then
    1.58      error ("Attempt to declare hidden name " ^ quote name)
    1.59    else
    1.60 -    let val names = unpack name in
    1.61 +    let val names = explode_name name in
    1.62        conditional (null names orelse exists (fn s => s = "") names) (fn () =>
    1.63          error ("Bad name declaration " ^ quote name));
    1.64 -      fold (add_name name) (map pack (accs names)) space
    1.65 +      fold (add_name name) (map implode_name (accs names)) space
    1.66      end;
    1.67  
    1.68  
    1.69 @@ -258,7 +258,7 @@
    1.70  
    1.71  fun sticky_prefix prfx (Naming (path, (qualify, _))) =
    1.72    Naming (append path prfx,
    1.73 -    (qualify, suffixes_prefixes_split (length (unpack path)) (length (unpack prfx))));
    1.74 +    (qualify, suffixes_prefixes_split (length (explode_name path)) (length (explode_name prfx))));
    1.75  
    1.76  fun set_policy policy (Naming (path, _)) = Naming (path, policy);
    1.77  
    1.78 @@ -284,6 +284,11 @@
    1.79  fun dest_table tab = map (apfst #1) (ext_table tab);
    1.80  fun extern_table tab = map (apfst #2) (ext_table tab);
    1.81  
    1.82 +
    1.83 +(*final declarations of this structure!*)
    1.84 +val implode = implode_name;
    1.85 +val explode = explode_name;
    1.86 +
    1.87  end;
    1.88  
    1.89  structure BasicNameSpace: BASIC_NAME_SPACE = NameSpace;