--- a/src/Tools/cache_io.ML Fri Nov 12 15:56:11 2010 +0100
+++ b/src/Tools/cache_io.ML Fri Nov 12 17:28:43 2010 +0100
@@ -9,18 +9,20 @@
(*IO wrapper*)
val with_tmp_file: string -> (Path.T -> 'a) -> 'a
val with_tmp_dir: string -> (Path.T -> 'a) -> 'a
- val run: (Path.T -> Path.T -> string) -> string ->
- {output: string list, redirected_output: string list, return_code: int}
+ type result = {
+ output: string list,
+ redirected_output: string list,
+ return_code: int}
+ val run: (Path.T -> Path.T -> string) -> string -> result
(*cache*)
type cache
val make: Path.T -> cache
val cache_path_of: cache -> Path.T
- val lookup: cache -> string -> (string list * string list) option * string
+ val lookup: cache -> string -> result option * string
val run_and_cache: cache -> string -> (Path.T -> Path.T -> string) ->
- string -> string list * string list
- val run_cached: cache -> (Path.T -> Path.T -> string) -> string ->
- string list * string list
+ string -> result
+ val run_cached: cache -> (Path.T -> Path.T -> string) -> string -> result
end
structure Cache_IO : CACHE_IO =
@@ -45,6 +47,11 @@
val _ = try File.rm_tree path
in Exn.release x end
+type result = {
+ output: string list,
+ redirected_output: string list,
+ return_code: int}
+
fun run make_cmd str =
with_tmp_file cache_io_prefix (fn in_path =>
with_tmp_file cache_io_prefix (fn out_path =>
@@ -98,7 +105,9 @@
else if i < p + len1 then (i+1, apfst (cons line) xsp)
else if i < p + len2 then (i+1, apsnd (cons line) xsp)
else (i, xsp)
- in pairself rev (snd (File.fold_lines load cache_path (1, ([], [])))) end
+ val (out, err) =
+ pairself rev (snd (File.fold_lines load cache_path (1, ([], []))))
+ in {output=err, redirected_output=out, return_code=0} end
fun lookup (Cache {path=cache_path, table}) str =
let val key = SHA1.digest str
@@ -110,9 +119,8 @@
fun run_and_cache (Cache {path=cache_path, table}) key make_cmd str =
let
- val {output=err, redirected_output=out, ...} = run make_cmd str
- val res = (out, err)
- val (l1, l2) = pairself length res
+ val {output=err, redirected_output=out, return_code} = run make_cmd str
+ val (l1, l2) = pairself length (out, err)
val header = key ^ " " ^ string_of_int l1 ^ " " ^ string_of_int l2
val lines = map (suffix "\n") (header :: out @ err)
@@ -121,7 +129,7 @@
else
let val _ = File.append_list cache_path lines
in (p+l1+l2+1, Symtab.update (key, (p+1, l1, l2)) tab) end)
- in res end
+ in {output=err, redirected_output=out, return_code=return_code} end
fun run_cached cache make_cmd str =
(case lookup cache str of