src/Pure/General/name_space.ML
changeset 20530 448594cbd82b
parent 19367 6af9ee48b563
child 21858 05f57309170c
     1.1 --- a/src/Pure/General/name_space.ML	Wed Sep 13 12:40:39 2006 +0200
     1.2 +++ b/src/Pure/General/name_space.ML	Wed Sep 13 21:41:25 2006 +0200
     1.3 @@ -27,7 +27,7 @@
     1.4    val append: string -> string -> string
     1.5    val qualified: string -> string -> string
     1.6    val base: string -> string
     1.7 -  val drop_base: string -> string
     1.8 +  val qualifier: string -> string
     1.9    val map_base: (string -> string) -> string -> string
    1.10    val suffixes_prefixes: 'a list -> 'a list list
    1.11    val suffixes_prefixes_split: int -> int -> 'a list -> 'a list list
    1.12 @@ -84,8 +84,8 @@
    1.13  fun base "" = ""
    1.14    | base name = List.last (unpack name);
    1.15  
    1.16 -fun drop_base "" = ""
    1.17 -  | drop_base name = pack (#1 (split_last (unpack name)));
    1.18 +fun qualifier "" = ""
    1.19 +  | qualifier name = pack (#1 (split_last (unpack name)));
    1.20  
    1.21  fun map_base _ "" = ""
    1.22    | map_base f name =
    1.23 @@ -248,7 +248,7 @@
    1.24  fun add_path elems (Naming (path, policy)) =
    1.25    if elems = "//" then Naming ("", (qualified, #2 policy))
    1.26    else if elems = "/" then Naming ("", policy)
    1.27 -  else if elems = ".." then Naming (drop_base path, policy)
    1.28 +  else if elems = ".." then Naming (qualifier path, policy)
    1.29    else Naming (append path elems, policy);
    1.30  
    1.31  fun no_base_names (Naming (path, (qualify, accs))) =