equal
deleted
inserted
replaced
79 let |
79 let |
80 fun err () = error ("Cache IO: corrupted cache file: " ^ |
80 fun err () = error ("Cache IO: corrupted cache file: " ^ |
81 File.shell_path cache_path) |
81 File.shell_path cache_path) |
82 |
82 |
83 fun int_of_string s = |
83 fun int_of_string s = |
84 (case read_int (explode s) of |
84 (case read_int (raw_explode s) of |
85 (i, []) => i |
85 (i, []) => i |
86 | _ => err ()) |
86 | _ => err ()) |
87 |
87 |
88 fun split line = |
88 fun split line = |
89 (case space_explode " " line of |
89 (case space_explode " " line of |