equal
deleted
inserted
replaced
33 type result = { |
33 type result = { |
34 output: string list, |
34 output: string list, |
35 redirected_output: string list, |
35 redirected_output: string list, |
36 return_code: int} |
36 return_code: int} |
37 |
37 |
|
38 val read_lines = Bytes.read #> Bytes.trim_split_lines |
|
39 |
38 fun raw_run make_cmd str in_path out_path = |
40 fun raw_run make_cmd str in_path out_path = |
39 let |
41 let |
40 val _ = File.write in_path str |
42 val _ = File.write in_path str |
41 val (out2, rc) = Isabelle_System.bash_output (make_cmd in_path out_path) |
43 val (out2, rc) = Isabelle_System.bash_output (make_cmd in_path out_path) |
42 val out1 = the_default [] (try (rev o File.fold_lines cons out_path) []) |
44 val out1 = the_default [] (try read_lines out_path) |
43 in {output = split_lines out2, redirected_output = out1, return_code = rc} end |
45 in {output = split_lines out2, redirected_output = out1, return_code = rc} end |
44 |
46 |
45 fun run make_cmd str = |
47 fun run make_cmd str = |
46 Isabelle_System.with_tmp_file cache_io_prefix "" (fn in_path => |
48 Isabelle_System.with_tmp_file cache_io_prefix "" (fn in_path => |
47 Isabelle_System.with_tmp_file cache_io_prefix "" (fn out_path => |
49 Isabelle_System.with_tmp_file cache_io_prefix "" (fn out_path => |
78 if i = l |
80 if i = l |
79 then |
81 then |
80 let val (key, l1, l2) = split line |
82 let val (key, l1, l2) = split line |
81 in ((i+1, l+l1+l2+1), Symtab.update (key, (i+1, l1, l2)) tab) end |
83 in ((i+1, l+l1+l2+1), Symtab.update (key, (i+1, l1, l2)) tab) end |
82 else ((i+1, l), tab) |
84 else ((i+1, l), tab) |
83 in apfst fst (File.fold_lines parse cache_path ((1, 1), Symtab.empty)) end |
85 in apfst fst (fold parse (read_lines cache_path) ((1, 1), Symtab.empty)) end |
84 else (1, Symtab.empty) |
86 else (1, Symtab.empty) |
85 in Cache {path = cache_path, table = Synchronized.var "Cache_IO" table} end |
87 in Cache {path = cache_path, table = Synchronized.var "Cache_IO" table} end |
86 |
88 |
87 fun lookup (Cache {path = cache_path, table}) str = |
89 fun lookup (Cache {path = cache_path, table}) str = |
88 let val key = SHA1.rep (SHA1.digest str) |
90 let val key = SHA1.rep (SHA1.digest str) |
96 if i < p then (i+1, xsp) |
98 if i < p then (i+1, xsp) |
97 else if i < p + len1 then (i+1, apfst (cons line) xsp) |
99 else if i < p + len1 then (i+1, apfst (cons line) xsp) |
98 else if i < p + len2 then (i+1, apsnd (cons line) xsp) |
100 else if i < p + len2 then (i+1, apsnd (cons line) xsp) |
99 else (i, xsp) |
101 else (i, xsp) |
100 val (out, err) = |
102 val (out, err) = |
101 apply2 rev (snd (File.fold_lines load cache_path (1, ([], [])))) |
103 apply2 rev (snd (fold load (read_lines cache_path) (1, ([], [])))) |
102 in ((SOME {output = err, redirected_output = out, return_code = 0}, key), tab) end)) |
104 in ((SOME {output = err, redirected_output = out, return_code = 0}, key), tab) end)) |
103 end |
105 end |
104 |
106 |
105 fun run_and_cache (Cache {path = cache_path, table}) key make_cmd str = |
107 fun run_and_cache (Cache {path = cache_path, table}) key make_cmd str = |
106 let |
108 let |