src/Pure/library.ML
changeset 1456 2e07cd051ff9
parent 1407 c22cc592785f
child 1458 fd510875fb71
     1.1 --- a/src/Pure/library.ML	Mon Jan 29 13:48:37 1996 +0100
     1.2 +++ b/src/Pure/library.ML	Mon Jan 29 13:49:17 1996 +0100
     1.3 @@ -738,6 +738,17 @@
     1.4      error "Relative or empty path passed to subdir_of"
     1.5    else (space_explode "/" path2) prefix (space_explode "/" path1);
     1.6  
     1.7 +fun absolute_path cwd file =
     1.8 +  let fun rm_points [] result = rev result
     1.9 +        | rm_points (".."::ds) result = rm_points ds (tl result)
    1.10 +        | rm_points ("."::ds) result = rm_points ds result
    1.11 +        | rm_points (d::ds) result = rm_points ds (d::result);
    1.12 +  in if file = "" then ""
    1.13 +     else if hd (explode file) = "/" then file
    1.14 +     else "/" ^ space_implode "/"
    1.15 +                  (rm_points (space_explode "/" (tack_on cwd file)) [])
    1.16 +  end;
    1.17 +
    1.18  
    1.19  (** misc functions **)
    1.20