src/Pure/General/file.ML

--- a/src/Pure/General/file.ML	Sat Nov 27 12:02:19 2010 +0100
+++ b/src/Pure/General/file.ML	Sat Nov 27 14:19:04 2010 +0100
@@ -14,9 +14,6 @@
   val full_path: Path.T -> Path.T
   val tmp_path: Path.T -> Path.T
   val isabelle_tool: string -> string -> int
-  eqtype ident
-  val rep_ident: ident -> string
-  val ident: Path.T -> ident option
   val exists: Path.T -> bool
   val check: Path.T -> unit
   val rm: Path.T -> unit
@@ -84,47 +81,6 @@
   else ();
 
 
-(* file identification *)
-
-local
-  val ident_cache =
-    Unsynchronized.ref (Symtab.empty: {time_stamp: string, id: string} Symtab.table);
-in
-
-fun check_cache (path, time) =
-  (case Symtab.lookup (! ident_cache) path of
-    NONE => NONE
-  | SOME {time_stamp, id} => if time_stamp = time then SOME id else NONE);
-
-fun update_cache (path, (time, id)) = CRITICAL (fn () =>
-  Unsynchronized.change ident_cache
-    (Symtab.update (path, {time_stamp = time, id = id})));
-
-end;
-
-datatype ident = Ident of string;
-fun rep_ident (Ident s) = s;
-
-fun ident path =
-  let val physical_path = perhaps (try OS.FileSys.fullPath) (platform_path path) in
-    (case try (Time.toString o OS.FileSys.modTime) physical_path of
-      NONE => NONE
-    | SOME mod_time => SOME (Ident
-        (case getenv "ISABELLE_FILE_IDENT" of
-          "" => physical_path ^ ": " ^ mod_time
-        | cmd =>
-            (case check_cache (physical_path, mod_time) of
-              SOME id => id
-            | NONE =>
-                let val (id, rc) =  (*potentially slow*)
-                  bash_output ("\"$ISABELLE_HOME/lib/scripts/fileident\" " ^ shell_quote physical_path)
-                in
-                  if id <> "" andalso rc = 0 then (update_cache (physical_path, (mod_time, id)); id)
-                  else error ("Failed to identify file " ^ quote (Path.implode path) ^ " by " ^ cmd)
-                end))))
-  end;
-
-
 (* directory entries *)
 
 val exists = can OS.FileSys.modTime o platform_path;