# HG changeset patch
# User wenzelm
# Date 1211115873 -7200
# Node ID 0b6eff8c088da9cee724f860404a2873652a8f9a
# Parent  9cd13e810998d61f75f0a32fe319a7325940b093
removed norm_absolute (not thread safe; chdir does not guarantee normalization anyway);
full_path: no link expansion here (reverted change of 1.18);
ident: OS.FileSys.fullPath takes care of link expansion;

diff -r 9cd13e810998 -r 0b6eff8c088d src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Sun May 18 15:04:31 2008 +0200
+++ b/src/Pure/General/file.ML	Sun May 18 15:04:33 2008 +0200
@@ -49,19 +49,9 @@
 val cd = cd o platform_path;
 val pwd = Path.explode o pwd;
 
-(* FIXME not thread-safe! *)
-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 =
-  (if Path.is_absolute path then path
-   else Path.append (pwd ()) path)
-  |> norm_absolute;
+  if Path.is_absolute path then path
+  else Path.append (pwd ()) path;
 
 
 (* tmp_path *)
@@ -86,18 +76,20 @@
 fun rep_ident (Ident s) = s;
 
 fun ident path =
-  (case try OS.FileSys.modTime (platform_path path) of
-    NONE => NONE
-  | SOME time => SOME (Ident
-      (case getenv "ISABELLE_FILE_IDENT" of
-        "" => Path.implode (full_path path) ^ ": " ^ Time.toString time
-      | cmd =>
-         let
-           val (id, rc) = system_out ("\"$ISABELLE_HOME/lib/scripts/fileident\" " ^ shell_path path)
-         in
-           if id <> "" andalso rc = 0 then id
-           else error ("Failed to identify file " ^ quote (Path.implode path) ^ " by " ^ cmd)
-         end)));
+  let val p = platform_path path in
+    (case try OS.FileSys.modTime p of
+      NONE => NONE
+    | SOME time => SOME (Ident
+        (case getenv "ISABELLE_FILE_IDENT" of
+          "" => OS.FileSys.fullPath p ^ ": " ^ Time.toString time
+        | cmd =>
+           let
+             val (id, rc) = system_out ("\"$ISABELLE_HOME/lib/scripts/fileident\" " ^ shell_path path)
+           in
+             if id <> "" andalso rc = 0 then id
+             else error ("Failed to identify file " ^ quote (Path.implode path) ^ " by " ^ cmd)
+           end)))
+  end;
 
 val exists = can OS.FileSys.modTime o platform_path;