src/Tools/cache_io.ML
changeset 35942 667fd8553cd5
parent 35941 63f0d628edff
child 36086 8e5454761f26
equal deleted inserted replaced
35941:63f0d628edff 35942:667fd8553cd5
     1 (*  Title:      Tools/Cache_IO/cache_io.ML
     1 (*  Title:      Tools/cache_io.ML
     2     Author:     Sascha Boehme, TU Muenchen
     2     Author:     Sascha Boehme, TU Muenchen
     3 
     3 
     4 Cache for output of external processes.
     4 Cache for output of external processes.
     5 *)
     5 *)
     6 
     6 
    74 fun make path =
    74 fun make path =
    75   let val table = if File.exists path then load path else (1, Symtab.empty)
    75   let val table = if File.exists path then load path else (1, Symtab.empty)
    76   in Cache {path=path, table=Synchronized.var (Path.implode path) table} end
    76   in Cache {path=path, table=Synchronized.var (Path.implode path) table} end
    77 
    77 
    78 
    78 
    79 fun get_hash_key path =
       
    80   let
       
    81     val arg = File.shell_path path
       
    82     val (out, res) = bash_output (getenv "COMPUTE_HASH_KEY" ^ " " ^ arg)
       
    83   in
       
    84     if res = 0 then hd (split_lines out)
       
    85     else error ("Cache IO: failed to generate hash key for file " ^ arg)
       
    86   end
       
    87 
       
    88 fun load_cached_result cache_path (p, len1, len2) =
    79 fun load_cached_result cache_path (p, len1, len2) =
    89   let
    80   let
    90     fun load line (i, xsp) =
    81     fun load line (i, xsp) =
    91       if i < p then (i+1, xsp)
    82       if i < p then (i+1, xsp)
    92       else if i < p + len1 then (i+1, apfst (cons line) xsp)
    83       else if i < p + len1 then (i+1, apfst (cons line) xsp)
    93       else if i < p + len2 then (i+1, apsnd (cons line) xsp)
    84       else if i < p + len2 then (i+1, apsnd (cons line) xsp)
    94       else (i, xsp)
    85       else (i, xsp)
    95   in pairself rev (snd (File.fold_lines load cache_path (1, ([], [])))) end
    86   in pairself rev (snd (File.fold_lines load cache_path (1, ([], [])))) end
    96 
    87 
    97 fun cached' (Cache {path=cache_path, table}) make_cmd in_path =
    88 fun cached' (Cache {path=cache_path, table}) make_cmd in_path =
    98   let val key = get_hash_key in_path
    89   let val key = SHA1.digest (File.read in_path)
    99   in
    90   in
   100     (case Symtab.lookup (snd (Synchronized.value table)) key of
    91     (case Symtab.lookup (snd (Synchronized.value table)) key of
   101       SOME pos => load_cached_result cache_path pos
    92       SOME pos => load_cached_result cache_path pos
   102     | NONE =>
    93     | NONE =>
   103         let
    94         let