src/Pure/Thy/thy_load.ML
changeset 41955 703ea96b13c6
parent 41944 b97091ae583a
child 42002 ac7097bd8611
--- a/src/Pure/Thy/thy_load.ML	Sun Mar 13 20:21:24 2011 +0100
+++ b/src/Pure/Thy/thy_load.ML	Sun Mar 13 20:56:00 2011 +0100
@@ -7,18 +7,15 @@
 
 signature THY_LOAD =
 sig
-  eqtype file_ident
-  val pretty_file_ident: file_ident -> Pretty.T
-  val file_ident: Path.T -> file_ident option
   val set_master_path: Path.T -> unit
   val get_master_path: unit -> Path.T
   val master_directory: theory -> Path.T
   val imports_of: theory -> string list
-  val provide: Path.T * (Path.T * file_ident) -> theory -> theory
-  val check_file: Path.T -> Path.T -> Path.T * file_ident
-  val check_thy: Path.T -> string -> Path.T * file_ident
+  val provide: Path.T * (Path.T * SHA1.digest) -> theory -> theory
+  val check_file: Path.T -> Path.T -> Path.T * SHA1.digest
+  val check_thy: Path.T -> string -> Path.T * SHA1.digest
   val deps_thy: Path.T -> string ->
-   {master: Path.T * file_ident, text: string, imports: string list, uses: Path.T list}
+   {master: Path.T * SHA1.digest, text: string, imports: string list, uses: Path.T list}
   val loaded_files: theory -> Path.T list
   val all_current: theory -> bool
   val provide_file: Path.T -> theory -> theory
@@ -30,58 +27,13 @@
 structure Thy_Load: THY_LOAD =
 struct
 
-(* file identification *)
-
-local
-  val file_ident_cache =
-    Synchronized.var "file_ident_cache"
-      (Symtab.empty: {time_stamp: string, id: string} Symtab.table);
-in
-
-fun check_cache (path, time) =
-  (case Symtab.lookup (Synchronized.value file_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)) =
-  Synchronized.change file_ident_cache
-    (Symtab.update (path, {time_stamp = time, id = id}));
-
-end;
-
-datatype file_ident = File_Ident of string;
-
-fun pretty_file_ident (File_Ident s) = Pretty.str (quote s);
-
-fun file_ident path =
-  let val physical_path = perhaps (try OS.FileSys.fullPath) (File.platform_path path) in
-    (case try (Time.toString o OS.FileSys.modTime) physical_path of
-      NONE => NONE
-    | SOME mod_time => SOME (File_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\" " ^ File.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 " ^ Path.print path ^ " by " ^ cmd)
-                end))))
-  end;
-
-
 (* manage source files *)
 
 type files =
  {master_dir: Path.T,  (*master directory of theory source*)
   imports: string list,  (*source specification of imports*)
   required: Path.T list,  (*source path*)
-  provided: (Path.T * (Path.T * file_ident)) list};  (*source path, physical path, identifier*)
+  provided: (Path.T * (Path.T * SHA1.digest)) list};  (*source path, physical path, digest*)
 
 fun make_files (master_dir, imports, required, provided): files =
  {master_dir = master_dir, imports = imports, required = required, provided = provided};
@@ -137,9 +89,9 @@
     val _ = Path.is_current path andalso error "Bad file specification";
     val full_path = File.full_path (Path.append dir path);
   in
-    (case file_ident full_path of
-      NONE => NONE
-    | SOME id => SOME (full_path, id))
+    if File.exists full_path
+    then SOME (full_path, SHA1.digest (File.read full_path))
+    else NONE
   end;
 
 fun check_file dir file =