# HG changeset patch
# User clasohm
# Date 822919757 -3600
# Node ID 2e07cd051ff9053ad19dd504e2b6df2b4377a752
# Parent  52a0271621f395ff2aa5b1d670430e1079b1a3b3
added absolute_path

diff -r 52a0271621f3 -r 2e07cd051ff9 src/Pure/library.ML
--- 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 **)