# HG changeset patch
# User berghofe
# Date 1093273578 -7200
# Node ID 6cdd6a8da9b9de2c0a98927922ce9b4d5f4ece9a
# Parent  db582d6e89de954c8cd0d9a50f8fa25a8fb1d151
Added function for "normalizing" absolute paths (i.e. dereferencing of
symbolic links; the functions in path.ML cannot do this). This is used
by function full_path.

diff -r db582d6e89de -r 6cdd6a8da9b9 src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Mon Aug 23 16:41:06 2004 +0200
+++ b/src/Pure/General/file.ML	Mon Aug 23 17:06:18 2004 +0200
@@ -49,9 +49,17 @@
 val cd = Library.cd o sysify_path;
 val pwd = unsysify_path o Library.pwd;
 
-fun full_path path =
-  if Path.is_absolute path then path
-  else Path.append (pwd ()) path;
+fun norm_absolute p =
+  let
+    val p' = pwd ();
+    fun norm p = if can cd p then pwd ()
+      else Path.append (norm (Path.dir p)) (Path.base p);
+    val p'' = norm p
+  in (cd p'; p'') end
+
+fun full_path path = norm_absolute
+  (if Path.is_absolute path then path
+   else Path.append (pwd ()) path);
 
 
 (* tmp_path *)