# 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() }) }