diff -r 95449e4b4bf6 -r bb8468ae414e src/Pure/System/isabelle_system.ML
--- a/src/Pure/System/isabelle_system.ML	Mon Dec 20 13:36:25 2010 +0100
+++ b/src/Pure/System/isabelle_system.ML	Mon Dec 20 14:44:00 2010 +0100
@@ -7,10 +7,11 @@
 signature ISABELLE_SYSTEM =
 sig
   val isabelle_tool: string -> string -> int
-  val rm_tree: Path.T -> unit
   val mkdirs: Path.T -> unit
   val mkdir: Path.T -> unit
   val copy_dir: Path.T -> Path.T -> unit
+  val with_tmp_file: string -> (Path.T -> 'a) -> 'a
+  val with_tmp_dir: string -> (Path.T -> 'a) -> 'a
 end;
 
 structure Isabelle_System: ISABELLE_SYSTEM =
@@ -37,8 +38,6 @@
 
 (* directory operations *)
 
-fun rm_tree path = system_command ("rm -r " ^ File.shell_path path);
-
 fun mkdirs path = system_command ("mkdir -p " ^ File.shell_path path);
 
 fun mkdir path =
@@ -48,5 +47,33 @@
   if File.eq (src, dst) then ()
   else (system_command ("cp -r -f " ^ File.shell_path src ^ "/. " ^ File.shell_path dst); ());
 
+
+(* unique tmp files *)
+
+local
+
+fun fresh_path name =
+  let
+    val path = File.tmp_path (Path.basic (name ^ serial_string ()));
+    val _ = File.exists path andalso
+      raise Fail ("Temporary file already exists: " ^ quote (Path.implode path));
+  in path end;
+
+fun rm_tree path = system_command ("rm -r -f " ^ File.shell_path path);
+
+in
+
+fun with_tmp_file name f =
+  let val path = fresh_path name
+  in Exn.release (Exn.capture f path before try File.rm path) end;
+
+fun with_tmp_dir name f =
+  let
+    val path = fresh_path name;
+    val _ = mkdirs path;
+  in Exn.release (Exn.capture f path before try rm_tree path) end;
+
 end;
 
+end;
+