replaced info by ident (for full identification, potentially content-based);
authorwenzelm
Thu Jul 19 23:18:45 2007 +0200 (2007-07-19)
changeset 2386172bb3494746f
parent 23860 31f5c9e43e57
child 23862 b1861768d8f4
replaced info by ident (for full identification, potentially content-based);
ident: invoke external lib/scripts/fileident, depending on ISABELLE_FILE_IDENT;
src/Pure/General/file.ML
     1.1 --- a/src/Pure/General/file.ML	Thu Jul 19 23:18:43 2007 +0200
     1.2 +++ b/src/Pure/General/file.ML	Thu Jul 19 23:18:45 2007 +0200
     1.3 @@ -19,8 +19,8 @@
     1.4    val tmp_path: Path.T -> Path.T
     1.5    val isatool: string -> int
     1.6    val system_command: string -> unit
     1.7 -  eqtype info
     1.8 -  val info: Path.T -> info option
     1.9 +  eqtype ident
    1.10 +  val ident: Path.T -> ident option
    1.11    val exists: Path.T -> bool
    1.12    val check: Path.T -> unit
    1.13    val rm: Path.T -> unit
    1.14 @@ -86,12 +86,21 @@
    1.15  
    1.16  (* directory entries *)
    1.17  
    1.18 -datatype info = Info of string;
    1.19 +datatype ident = Ident of string;
    1.20  
    1.21 -fun info path =
    1.22 -  Option.map (Info o Time.toString) (try OS.FileSys.modTime (platform_path path));
    1.23 +fun ident path =
    1.24 +  (case try OS.FileSys.modTime (platform_path path) of
    1.25 +    NONE => NONE
    1.26 +  | SOME time => SOME (Ident
    1.27 +      (case getenv "ISABELLE_FILE_IDENT" of
    1.28 +        "" => Path.implode (full_path path) ^ ": " ^ Time.toString time
    1.29 +      | cmd =>
    1.30 +         let val id = execute ("\"$ISABELLE_HOME/lib/scripts/fileident\" " ^ shell_path path) in
    1.31 +           if id <> "" then id
    1.32 +           else error ("Failed to identify file " ^ quote (Path.implode path) ^ " by " ^ cmd)
    1.33 +         end)));
    1.34  
    1.35 -val exists = is_some o info;
    1.36 +val exists = can OS.FileSys.modTime o platform_path;
    1.37  
    1.38  fun check path =
    1.39    if exists path then ()