src/Pure/General/path.ML
changeset 40627 becf5d5187cc
parent 36135 89d1903fbd50
child 41944 b97091ae583a
     1.1 --- a/src/Pure/General/path.ML	Fri Nov 19 23:48:07 2010 +0100
     1.2 +++ b/src/Pure/General/path.ML	Sat Nov 20 00:53:26 2010 +0100
     1.3 @@ -73,9 +73,9 @@
     1.4  
     1.5  val current = Path [];
     1.6  val root = Path [Root ""];
     1.7 -fun named_root s = Path [root_elem (explode s)];
     1.8 -fun basic s = Path [basic_elem (explode s)];
     1.9 -fun variable s = Path [variable_elem (explode s)];
    1.10 +fun named_root s = Path [root_elem (raw_explode s)];
    1.11 +fun basic s = Path [basic_elem (raw_explode s)];
    1.12 +fun variable s = Path [variable_elem (raw_explode s)];
    1.13  val parent = Path [Parent];
    1.14  
    1.15  fun is_absolute (Path xs) =
    1.16 @@ -128,7 +128,7 @@
    1.17    | explode_elem "~" = Variable "HOME"
    1.18    | explode_elem "~~" = Variable "ISABELLE_HOME"
    1.19    | explode_elem s =
    1.20 -      (case explode s of
    1.21 +      (case raw_explode s of
    1.22          "$" :: cs => variable_elem cs
    1.23        | cs => basic_elem cs);
    1.24  
    1.25 @@ -143,7 +143,7 @@
    1.26        (0, es) => ([], es)
    1.27      | (1, es) => ([Root ""], es)
    1.28      | (_, []) => ([Root ""], [])
    1.29 -    | (_, e :: es) => ([root_elem (explode e)], es))
    1.30 +    | (_, e :: es) => ([root_elem (raw_explode e)], es))
    1.31    in Path (norm (explode_elems raw_elems @ roots)) end;
    1.32  
    1.33  end;
    1.34 @@ -161,7 +161,7 @@
    1.35    | ext e = split_path (fn (prfx, s) => append prfx (basic (s ^ "." ^ e)));
    1.36  
    1.37  val split_ext = split_path (fn (prfx, s) => apfst (append prfx)
    1.38 -  (case take_suffix (fn c => c <> ".") (explode s) of
    1.39 +  (case take_suffix (fn c => c <> ".") (raw_explode s) of
    1.40      ([], _) => (Path [Basic s], "")
    1.41    | (cs, e) => (Path [Basic (implode (take (length cs - 1) cs))], implode e)));
    1.42