# HG changeset patch
# User wenzelm
# Date 1262015101 -3600
# Node ID c352f679dccac5be9f0c0b08ea3882d6c4cd74b5
# Parent  d58da36d1a30731d06d14a15fb49f08eb2c32cf7
higher-order treatment of temporary files;

diff -r d58da36d1a30 -r c352f679dcca src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Mon Dec 28 16:24:19 2009 +0100
+++ b/src/Pure/System/isabelle_system.scala	Mon Dec 28 16:45:01 2009 +0100
@@ -90,8 +90,7 @@
         case Some(path) => path
       }
 
-    val dump = File.createTempFile("isabelle", null)
-    try {
+    Library.with_tmp_file("isabelle_settings") { dump =>
       val cmdline = shell_prefix :::
         List(isabelle_home + "/bin/isabelle", "getenv", "-d", dump.toString)
       val (output, rc) =
@@ -108,7 +107,6 @@
         ("HOME" -> java.lang.System.getenv("HOME")) +
         ("PATH" -> java.lang.System.getenv("PATH"))
     }
-    finally { dump.delete }
   }
 
 
diff -r d58da36d1a30 -r c352f679dcca src/Pure/library.scala
--- a/src/Pure/library.scala	Mon Dec 28 16:24:19 2009 +0100
+++ b/src/Pure/library.scala	Mon Dec 28 16:45:01 2009 +0100
@@ -7,6 +7,7 @@
 package isabelle
 
 import java.lang.System
+import java.io.File
 
 
 object Library
@@ -82,6 +83,18 @@
   }
 
 
+  /* temporary file */
+
+  def with_tmp_file[A](prefix: String)(body: File => A): A =
+  {
+    val file = File.createTempFile(prefix, null)
+    val result =
+      try { body(file) }
+      finally { file.delete }
+    result
+  }
+
+
   /* timing */
 
   def timeit[A](e: => A) =