src/Pure/General/file.ML
changeset 26220 d34b68c21f9a
parent 24446 bb7a85ea57cf
child 26503 4dec4460244f
equal deleted inserted replaced
26219:2d026932f710 26220:d34b68c21f9a
    96     NONE => NONE
    96     NONE => NONE
    97   | SOME time => SOME (Ident
    97   | SOME time => SOME (Ident
    98       (case getenv "ISABELLE_FILE_IDENT" of
    98       (case getenv "ISABELLE_FILE_IDENT" of
    99         "" => Path.implode (full_path path) ^ ": " ^ Time.toString time
    99         "" => Path.implode (full_path path) ^ ": " ^ Time.toString time
   100       | cmd =>
   100       | cmd =>
   101          let val id = execute ("\"$ISABELLE_HOME/lib/scripts/fileident\" " ^ shell_path path) in
   101          let
   102            if id <> "" then id
   102            val (id, rc) = system_out ("\"$ISABELLE_HOME/lib/scripts/fileident\" " ^ shell_path path)
       
   103          in
       
   104            if id <> "" andalso rc = 0 then id
   103            else error ("Failed to identify file " ^ quote (Path.implode path) ^ " by " ^ cmd)
   105            else error ("Failed to identify file " ^ quote (Path.implode path) ^ " by " ^ cmd)
   104          end)));
   106          end)));
   105 
   107 
   106 val exists = can OS.FileSys.modTime o platform_path;
   108 val exists = can OS.FileSys.modTime o platform_path;
   107 
   109