src/Pure/General/name_space.ML
changeset 30359 3f9b3ff851ca
parent 30280 eb98b49ef835
child 30412 7f5b0a020ccd
     1.1 --- a/src/Pure/General/name_space.ML	Sun Mar 08 15:01:10 2009 +0100
     1.2 +++ b/src/Pure/General/name_space.ML	Sun Mar 08 16:53:07 2009 +0100
     1.3 @@ -19,15 +19,6 @@
     1.4    include BASIC_NAME_SPACE
     1.5    val hidden: string -> string
     1.6    val is_hidden: string -> bool
     1.7 -  val separator: string                 (*single char*)
     1.8 -  val is_qualified: string -> bool
     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_name: string -> string
    1.14 -  val qualifier: string -> string
    1.15 -  val map_base_name: (string -> string) -> string -> string
    1.16    type T
    1.17    val empty: T
    1.18    val intern: T -> xstring -> string
    1.19 @@ -64,32 +55,6 @@
    1.20  fun hidden name = "??." ^ name;
    1.21  val is_hidden = String.isPrefix "??.";
    1.22  
    1.23 -val separator = ".";
    1.24 -val is_qualified = exists_string (fn s => s = separator);
    1.25 -
    1.26 -val implode_name = space_implode separator;
    1.27 -val explode_name = space_explode separator;
    1.28 -
    1.29 -fun append name1 "" = name1
    1.30 -  | append "" name2 = name2
    1.31 -  | append name1 name2 = name1 ^ separator ^ name2;
    1.32 -
    1.33 -fun qualified path name =
    1.34 -  if path = "" orelse name = "" then name
    1.35 -  else path ^ separator ^ name;
    1.36 -
    1.37 -fun base_name "" = ""
    1.38 -  | base_name name = List.last (explode_name name);
    1.39 -
    1.40 -fun qualifier "" = ""
    1.41 -  | qualifier name = implode_name (#1 (split_last (explode_name name)));
    1.42 -
    1.43 -fun map_base_name _ "" = ""
    1.44 -  | map_base_name f name =
    1.45 -      let val names = explode_name name
    1.46 -      in implode_name (nth_map (length names - 1) f names) end;
    1.47 -
    1.48 -
    1.49  (* standard accesses *)
    1.50  
    1.51  infixr 6 @@;
    1.52 @@ -161,7 +126,7 @@
    1.53        | ext (nm :: nms) = if valid unique_names nm then nm else ext nms;
    1.54    in
    1.55      if long_names then name
    1.56 -    else if short_names then base_name name
    1.57 +    else if short_names then Long_Name.base_name name
    1.58      else ext (get_accesses space name)
    1.59    end;
    1.60  
    1.61 @@ -196,7 +161,7 @@
    1.62  (* hide *)
    1.63  
    1.64  fun hide fully name space =
    1.65 -  if not (is_qualified name) then
    1.66 +  if not (Long_Name.is_qualified name) then
    1.67      error ("Attempt to hide global name " ^ quote name)
    1.68    else if is_hidden name then
    1.69      error ("Attempt to hide hidden name " ^ quote name)
    1.70 @@ -204,7 +169,8 @@
    1.71      let val names = valid_accesses space name in
    1.72        space
    1.73        |> add_name' name name
    1.74 -      |> fold (del_name name) (if fully then names else names inter_string [base_name name])
    1.75 +      |> fold (del_name name)
    1.76 +        (if fully then names else names inter_string [Long_Name.base_name name])
    1.77        |> fold (del_name_extra name) (get_accesses space name)
    1.78      end;
    1.79  
    1.80 @@ -237,33 +203,34 @@
    1.81  fun path_of (Naming (path, _)) = path;
    1.82  fun accesses (Naming (_, (_, accs))) = accs;
    1.83  
    1.84 -fun external_names naming = map implode_name o #2 o accesses naming o explode_name;
    1.85 +fun external_names naming = map Long_Name.implode o #2 o accesses naming o Long_Name.explode;
    1.86  
    1.87  
    1.88  (* manipulate namings *)
    1.89  
    1.90  fun reject_qualified name =
    1.91 -  if is_qualified name then
    1.92 +  if Long_Name.is_qualified name then
    1.93      error ("Attempt to declare qualified name " ^ quote name)
    1.94    else name;
    1.95  
    1.96  val default_naming =
    1.97 -  Naming ("", (fn path => qualified path o reject_qualified, suffixes_prefixes));
    1.98 +  Naming ("", (fn path => Long_Name.qualify path o reject_qualified, suffixes_prefixes));
    1.99  
   1.100  fun add_path elems (Naming (path, policy)) =
   1.101 -  if elems = "//" then Naming ("", (qualified, #2 policy))
   1.102 +  if elems = "//" then Naming ("", (Long_Name.qualify, #2 policy))
   1.103    else if elems = "/" then Naming ("", policy)
   1.104 -  else if elems = ".." then Naming (qualifier path, policy)
   1.105 -  else Naming (append path elems, policy);
   1.106 +  else if elems = ".." then Naming (Long_Name.qualifier path, policy)
   1.107 +  else Naming (Long_Name.append path elems, policy);
   1.108  
   1.109  fun no_base_names (Naming (path, (qualify, accs))) =
   1.110    Naming (path, (qualify, pairself (filter_out (fn [_] => true | _ => false)) o accs));
   1.111  
   1.112 -fun qualified_names (Naming (path, (_, accs))) = Naming (path, (qualified, accs));
   1.113 +fun qualified_names (Naming (path, (_, accs))) = Naming (path, (Long_Name.qualify, accs));
   1.114  
   1.115  fun sticky_prefix prfx (Naming (path, (qualify, _))) =
   1.116 -  Naming (append path prfx,
   1.117 -    (qualify, suffixes_prefixes_split (length (explode_name path)) (length (explode_name prfx))));
   1.118 +  Naming (Long_Name.append path prfx,
   1.119 +    (qualify,
   1.120 +      suffixes_prefixes_split (length (Long_Name.explode path)) (length (Long_Name.explode prfx))));
   1.121  
   1.122  val apply_prefix =
   1.123    let
   1.124 @@ -290,13 +257,13 @@
   1.125      val (prfx, bname) = Binding.dest binding;
   1.126      val naming' = apply_prefix prfx naming;
   1.127      val name = full naming' bname;
   1.128 -    val names = explode_name name;
   1.129 +    val names = Long_Name.explode name;
   1.130  
   1.131      val _ = (null names orelse exists (fn s => s = "" orelse s = "??") names
   1.132          orelse exists_string (fn s => s = "\"") name) andalso
   1.133        error ("Bad name declaration " ^ quote (Binding.str_of binding));
   1.134  
   1.135 -    val (accs, accs') = pairself (map implode_name) (accesses naming' names);
   1.136 +    val (accs, accs') = pairself (map Long_Name.implode) (accesses naming' names);
   1.137      val space' = space |> fold (add_name name) accs |> put_accesses name accs';
   1.138    in (name, space') end;
   1.139  
   1.140 @@ -325,11 +292,6 @@
   1.141  fun dest_table tab = map (apfst #1) (ext_table tab);
   1.142  fun extern_table tab = map (apfst #2) (ext_table tab);
   1.143  
   1.144 -
   1.145 -(*final declarations of this structure!*)
   1.146 -val implode = implode_name;
   1.147 -val explode = explode_name;
   1.148 -
   1.149  end;
   1.150  
   1.151  structure BasicNameSpace: BASIC_NAME_SPACE = NameSpace;