src/Pure/library.ML
changeset 1456 2e07cd051ff9
parent 1407 c22cc592785f
child 1458 fd510875fb71
--- 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 **)