--- a/src/Tools/cache_io.ML Sun Mar 13 19:27:39 2011 +0100
+++ b/src/Tools/cache_io.ML Sun Mar 13 20:21:24 2011 +0100
@@ -67,7 +67,7 @@
fun int_of_string s =
(case read_int (raw_explode s) of
(i, []) => i
- | _ => err ())
+ | _ => err ())
fun split line =
(case space_explode " " line of
@@ -80,7 +80,7 @@
let val (key, l1, l2) = split line
in ((i+1, l+l1+l2+1), Symtab.update (key, (i+1, l1, l2)) tab) end
else ((i+1, l), tab)
- in apfst fst (File.fold_lines parse cache_path ((1, 1), Symtab.empty)) end
+ in apfst fst (File.fold_lines parse cache_path ((1, 1), Symtab.empty)) end
fun make path =
let val table = if File.exists path then load path else (1, Symtab.empty)
@@ -98,7 +98,7 @@
in {output=err, redirected_output=out, return_code=0} end
fun lookup (Cache {path=cache_path, table}) str =
- let val key = SHA1.digest str
+ let val key = SHA1.rep (SHA1.digest str)
in
(case Symtab.lookup (snd (Synchronized.value table)) key of
NONE => (NONE, key)