1.1 --- a/src/Pure/General/file.ML	Mon Aug 23 16:41:06 2004 +0200
     1.2 +++ b/src/Pure/General/file.ML	Mon Aug 23 17:06:18 2004 +0200
     1.3 @@ -49,9 +49,17 @@
     1.4  val cd = Library.cd o sysify_path;
     1.5  val pwd = unsysify_path o Library.pwd;
     1.6  
     1.7 -fun full_path path =
     1.8 -  if Path.is_absolute path then path
     1.9 -  else Path.append (pwd ()) path;
    1.10 +fun norm_absolute p =
    1.11 +  let
    1.12 +    val p' = pwd ();
    1.13 +    fun norm p = if can cd p then pwd ()
    1.14 +      else Path.append (norm (Path.dir p)) (Path.base p);
    1.15 +    val p'' = norm p
    1.16 +  in (cd p'; p'') end
    1.17 +
    1.18 +fun full_path path = norm_absolute
    1.19 +  (if Path.is_absolute path then path
    1.20 +   else Path.append (pwd ()) path);
    1.21  
    1.22  
    1.23  (* tmp_path *)