diff -r 5c6225a1c2c0 -r 2b098a549450 src/Tools/cache_io.ML
--- a/src/Tools/cache_io.ML	Tue Nov 16 12:08:28 2010 -0800
+++ b/src/Tools/cache_io.ML	Wed Nov 17 08:14:55 2010 +0100
@@ -13,6 +13,8 @@
     output: string list,
     redirected_output: string list,
     return_code: int}
+  val raw_run: (Path.T -> Path.T -> string) -> string -> Path.T -> Path.T ->
+    result
   val run: (Path.T -> Path.T -> string) -> string -> result
 
   (*cache*)
@@ -52,14 +54,16 @@
   redirected_output: string list,
   return_code: int}
 
+fun raw_run make_cmd str in_path out_path =
+  let
+    val _ = File.write in_path str
+    val (out2, rc) = bash_output (make_cmd in_path out_path)
+    val out1 = the_default [] (try (rev o File.fold_lines cons out_path) [])
+  in {output=split_lines out2, redirected_output=out1, return_code=rc} end
+
 fun run make_cmd str =
   with_tmp_file cache_io_prefix (fn in_path =>
-  with_tmp_file cache_io_prefix (fn out_path =>
-    let
-      val _ = File.write in_path str
-      val (out2, rc) = bash_output (make_cmd in_path out_path)
-      val out1 = the_default [] (try (rev o File.fold_lines cons out_path) [])
-    in {output=split_lines out2, redirected_output=out1, return_code=rc} end))
+  with_tmp_file cache_io_prefix (raw_run make_cmd str in_path))
 
 
 (* cache *)