diff -r 0eaa6905590f -r 8e5454761f26 src/Tools/cache_io.ML
--- a/src/Tools/cache_io.ML	Wed Apr 07 20:40:42 2010 +0200
+++ b/src/Tools/cache_io.ML	Wed Apr 07 20:40:42 2010 +0200
@@ -7,20 +7,23 @@
 signature CACHE_IO =
 sig
   val with_tmp_file: string -> (Path.T -> 'a) -> 'a
-  val run: (Path.T -> string) -> Path.T -> string list
-  val run': (Path.T -> Path.T -> string) -> Path.T -> string list * string list
+  val run: (Path.T -> Path.T -> string) -> string -> string list * string list
 
   type cache
   val make: Path.T -> cache
   val cache_path_of: cache -> Path.T
-  val cached: cache -> (Path.T -> string) -> Path.T -> string list
-  val cached': cache -> (Path.T -> Path.T -> string) -> Path.T ->
+  val lookup: cache -> string -> (string list * string list) 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
 end
 
 structure Cache_IO : CACHE_IO =
 struct
 
+val cache_io_prefix = "cache-io-"
+
 fun with_tmp_file name f =
   let
     val path = File.tmp_path (Path.explode (name ^ serial_string ()))
@@ -28,14 +31,14 @@
     val _ = try File.rm path
   in Exn.release x end
 
-fun run' make_cmd in_path =
-  with_tmp_file "cache-io-" (fn out_path =>
+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, _) = bash_output (make_cmd in_path out_path)
       val out1 = the_default [] (try (rev o File.fold_lines cons out_path) [])
-    in (out1, split_lines out2) end)
-
-fun run make_cmd = snd o run' (fn in_path => fn _ => make_cmd in_path)
+    in (out1, split_lines out2) end))
 
 
 
@@ -85,28 +88,35 @@
       else (i, xsp)
   in pairself rev (snd (File.fold_lines load cache_path (1, ([], [])))) end
 
-fun cached' (Cache {path=cache_path, table}) make_cmd in_path =
-  let val key = SHA1.digest (File.read in_path)
+
+fun lookup (Cache {path=cache_path, table}) str =
+  let val key = SHA1.digest str
   in
     (case Symtab.lookup (snd (Synchronized.value table)) key of
-      SOME pos => load_cached_result cache_path pos
-    | NONE =>
-        let
-          val res as (out, err) = run' make_cmd in_path
-          val (l1, l2) = pairself length res
-          val header = key ^ " " ^ string_of_int l1 ^ " " ^ string_of_int l2
-          val lines = map (suffix "\n") (header :: out @ err)
-
-          val _ = Synchronized.change table (fn (p, tab) =>
-            if Symtab.defined tab key then (p, tab)
-            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)
+      NONE => (NONE, key)
+    | SOME pos => (SOME (load_cached_result cache_path pos), key))
   end
 
-fun cached cache make_cmd =
-  snd o cached' cache (fn in_path => fn _ => make_cmd in_path)
+
+fun run_and_cache (Cache {path=cache_path, table}) key make_cmd str =
+  let
+    val res as (out, err) = run make_cmd str
+    val (l1, l2) = pairself length res
+    val header = key ^ " " ^ string_of_int l1 ^ " " ^ string_of_int l2
+    val lines = map (suffix "\n") (header :: out @ err)
+
+    val _ = Synchronized.change table (fn (p, tab) =>
+      if Symtab.defined tab key then (p, tab)
+      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
+
+
+fun run_cached cache make_cmd str =
+  (case lookup cache str of
+    (NONE, key) => run_and_cache cache key make_cmd str
+  | (SOME output, _) => output)
 
 end
 end