src/Pure/General/file.scala

--- a/src/Pure/General/file.scala	Sat Jul 21 12:57:31 2012 +0200
+++ b/src/Pure/General/file.scala	Sat Jul 21 16:41:55 2012 +0200
@@ -83,10 +83,16 @@
 
   /* misc */
 
-  def with_tmp_file[A](prefix: String)(body: JFile => A): A =
+  def tmp_file(prefix: String): JFile =
   {
     val file = JFile.createTempFile(prefix, null)
     file.deleteOnExit
+    file
+  }
+
+  def with_tmp_file[A](prefix: String)(body: JFile => A): A =
+  {
+    val file = tmp_file(prefix)
     try { body(file) } finally { file.delete }
   }