# HG changeset patch
# User wenzelm
# Date 1457816556 -3600
# Node ID c077eb5e0b56d73d627bb078e51dcf5975bcbfa1
# Parent  96e679f042eca8bf99b74b2eacd9467afa9cabdc
clarified cleanup;

diff -r 96e679f042ec -r c077eb5e0b56 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sat Mar 12 21:46:31 2016 +0100
+++ b/src/Pure/Tools/build.scala	Sat Mar 12 22:02:36 2016 +0100
@@ -553,9 +553,6 @@
 
     private val env = Map("ISABELLE_ML_DEBUGGER" -> info.options.bool("ML_debugger").toString)
 
-    private val args_file =
-      if (is_pure(name)) None else Some(Isabelle_System.tmp_file("args"))
-
     private val future_result: Future[Process_Result] =
       Future.thread("build") {
         val process =
@@ -568,7 +565,8 @@
               cwd = info.dir.file, env = env)
           }
           else {
-            File.write(args_file.get, YXML.string_of_body(
+            val args_file = Isabelle_System.tmp_file("build")
+            File.write(args_file, YXML.string_of_body(
                 {
                   val theories = info.theories.map(x => (x._2, x._3))
                   import XML.Encode._
@@ -582,9 +580,10 @@
                     theories)))))))))))
                 }))
             ML_Process(info.options, parent,
-              List("--eval", "Build.build " +
-                ML_Syntax.print_string_raw(File.standard_path(args_file.get))),
-              cwd = info.dir.file, env = env)
+              List("--eval",
+                "Build.build " + ML_Syntax.print_string_raw(File.standard_path(args_file))),
+              cwd = info.dir.file, env = env,
+              cleanup = () => args_file.delete)
           }
         process.result(
           progress_stdout = (line: String) =>
@@ -619,7 +618,6 @@
         Present.finish(progress, browser_info, graph_file, info, name)
 
       graph_file.delete
-      args_file.foreach(_.delete)
       timeout_request.foreach(_.cancel)
 
       if (result.interrupted) {
diff -r 96e679f042ec -r c077eb5e0b56 src/Pure/Tools/ml_process.scala
--- a/src/Pure/Tools/ml_process.scala	Sat Mar 12 21:46:31 2016 +0100
+++ b/src/Pure/Tools/ml_process.scala	Sat Mar 12 22:02:36 2016 +0100
@@ -20,6 +20,7 @@
     cwd: JFile = null,
     env: Map[String, String] = Map.empty,
     redirect: Boolean = false,
+    cleanup: () => Unit = () => (),
     channel: Option[System_Channel] = None): Bash.Process =
   {
     val load_heaps =
@@ -107,6 +108,7 @@
         {
           isabelle_process_options.delete
           Isabelle_System.rm_tree(isabelle_tmp)
+          cleanup()
         })
   }