1.1 --- a/src/Tools/cache_io.ML	Thu Jul 08 09:36:22 2010 +0200
     1.2 +++ b/src/Tools/cache_io.ML	Thu Jul 08 09:36:23 2010 +0200
     1.3 @@ -7,6 +7,7 @@
     1.4  signature CACHE_IO =
     1.5  sig
     1.6    val with_tmp_file: string -> (Path.T -> 'a) -> 'a
     1.7 +  val with_tmp_dir: string -> (Path.T -> 'a) -> 'a
     1.8    val run: (Path.T -> Path.T -> string) -> string -> string list * string list
     1.9  
    1.10    type cache
    1.11 @@ -31,6 +32,14 @@
    1.12      val _ = try File.rm path
    1.13    in Exn.release x end
    1.14  
    1.15 +fun with_tmp_dir name f =
    1.16 +  let
    1.17 +    val path = File.tmp_path (Path.explode (name ^ serial_string ()))
    1.18 +    val _ = File.mkdir path
    1.19 +    val x = Exn.capture f path
    1.20 +    val _ = try File.rm_tree path
    1.21 +  in Exn.release x end
    1.22 +
    1.23  fun run make_cmd str =
    1.24    with_tmp_file cache_io_prefix (fn in_path =>
    1.25    with_tmp_file cache_io_prefix (fn out_path =>