equal
deleted
inserted
replaced
82 else ((i+1, l), tab) |
82 else ((i+1, l), tab) |
83 in apfst fst (File.fold_lines parse cache_path ((1, 1), Symtab.empty)) end |
83 in apfst fst (File.fold_lines parse cache_path ((1, 1), Symtab.empty)) end |
84 |
84 |
85 fun make path = |
85 fun make path = |
86 let val table = if File.exists path then load path else (1, Symtab.empty) |
86 let val table = if File.exists path then load path else (1, Symtab.empty) |
87 in Cache {path=path, table=Synchronized.var (Path.implode path) table} end |
87 in Cache {path=path, table=Synchronized.var "Cache_IO" table} end |
88 |
88 |
89 fun load_cached_result cache_path (p, len1, len2) = |
89 fun load_cached_result cache_path (p, len1, len2) = |
90 let |
90 let |
91 fun load line (i, xsp) = |
91 fun load line (i, xsp) = |
92 if i < p then (i+1, xsp) |
92 if i < p then (i+1, xsp) |