--- a/src/Pure/library.ML Mon Jan 29 13:48:37 1996 +0100
+++ b/src/Pure/library.ML Mon Jan 29 13:49:17 1996 +0100
@@ -738,6 +738,17 @@
error "Relative or empty path passed to subdir_of"
else (space_explode "/" path2) prefix (space_explode "/" path1);
+fun absolute_path cwd file =
+ let fun rm_points [] result = rev result
+ | rm_points (".."::ds) result = rm_points ds (tl result)
+ | rm_points ("."::ds) result = rm_points ds result
+ | rm_points (d::ds) result = rm_points ds (d::result);
+ in if file = "" then ""
+ else if hd (explode file) = "/" then file
+ else "/" ^ space_implode "/"
+ (rm_points (space_explode "/" (tack_on cwd file)) [])
+ end;
+
(** misc functions **)