96 if i < p then (i+1, xsp) |
96 if i < p then (i+1, xsp) |
97 else if i < p + len1 then (i+1, apfst (cons line) xsp) |
97 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) |
98 else if i < p + len2 then (i+1, apsnd (cons line) xsp) |
99 else (i, xsp) |
99 else (i, xsp) |
100 val (out, err) = |
100 val (out, err) = |
101 pairself rev (snd (File.fold_lines load cache_path (1, ([], [])))) |
101 apply2 rev (snd (File.fold_lines load cache_path (1, ([], [])))) |
102 in ((SOME {output = err, redirected_output = out, return_code = 0}, key), tab) end)) |
102 in ((SOME {output = err, redirected_output = out, return_code = 0}, key), tab) end)) |
103 end |
103 end |
104 |
104 |
105 fun run_and_cache (Cache {path = cache_path, table}) key make_cmd str = |
105 fun run_and_cache (Cache {path = cache_path, table}) key make_cmd str = |
106 let |
106 let |
107 val {output = err, redirected_output=out, return_code} = run make_cmd str |
107 val {output = err, redirected_output=out, return_code} = run make_cmd str |
108 val (l1, l2) = pairself length (out, err) |
108 val (l1, l2) = apply2 length (out, err) |
109 val header = key ^ " " ^ string_of_int l1 ^ " " ^ string_of_int l2 |
109 val header = key ^ " " ^ string_of_int l1 ^ " " ^ string_of_int l2 |
110 val lines = map (suffix "\n") (header :: out @ err) |
110 val lines = map (suffix "\n") (header :: out @ err) |
111 |
111 |
112 val _ = Synchronized.change table (fn (p, tab) => |
112 val _ = Synchronized.change table (fn (p, tab) => |
113 if Symtab.defined tab key then (p, tab) |
113 if Symtab.defined tab key then (p, tab) |