add_path: discontinued special meaning of "//", "/", "..";
authorwenzelm
Tue Mar 10 21:18:01 2009 +0100 (2009-03-10)
changeset 30418b5044aca0729
parent 30417 09a757ca128f
child 30419 c944e299eaf9
add_path: discontinued special meaning of "//", "/", "..";
added root_path, parent_path;
src/Pure/General/name_space.ML
     1.1 --- a/src/Pure/General/name_space.ML	Tue Mar 10 18:52:26 2009 +0100
     1.2 +++ b/src/Pure/General/name_space.ML	Tue Mar 10 21:18:01 2009 +0100
     1.3 @@ -33,6 +33,8 @@
     1.4    val full_name: naming -> binding -> string
     1.5    val external_names: naming -> string -> string list
     1.6    val add_path: string -> naming -> naming
     1.7 +  val root_path: naming -> naming
     1.8 +  val parent_path: naming -> naming
     1.9    val no_base_names: naming -> naming
    1.10    val qualified_names: naming -> naming
    1.11    val sticky_prefix: string -> naming -> naming
    1.12 @@ -189,10 +191,13 @@
    1.13  val default_naming = make_naming ([], false, false);
    1.14  
    1.15  fun add_path elems = map_naming (fn (path, no_base_names, qualified_names) =>
    1.16 -  if elems = "//" then ([], no_base_names, true)
    1.17 -  else if elems = "/" then ([], no_base_names, qualified_names)
    1.18 -  else if elems = ".." then (perhaps (try (#1 o split_last)) path, no_base_names, qualified_names)
    1.19 -  else (path @ map (rpair false) (Long_Name.explode elems), no_base_names, qualified_names));
    1.20 +  (path @ map (rpair false) (Long_Name.explode elems), no_base_names, qualified_names));
    1.21 +
    1.22 +val root_path = map_naming (fn (_, no_base_names, qualified_names) =>
    1.23 +  ([], no_base_names, qualified_names));
    1.24 +
    1.25 +val parent_path = map_naming (fn (path, no_base_names, qualified_names) =>
    1.26 +  (perhaps (try (#1 o split_last)) path, no_base_names, qualified_names));
    1.27  
    1.28  fun sticky_prefix elems = map_naming (fn (path, no_base_names, qualified_names) =>
    1.29    (path @ map (rpair true) (Long_Name.explode elems), no_base_names, qualified_names));