avoid race condition wrt. ISABELLE_TMP, which is removed in Bash.cleanup() before Bash.result(progress_stdout);
--- a/src/Pure/Tools/build.ML Wed May 16 21:07:12 2018 +0200
+++ b/src/Pure/Tools/build.ML Wed May 16 21:36:59 2018 +0200
@@ -98,10 +98,9 @@
not (null args) andalso #1 (hd args) = Markup.idN
then
let
- val path = Isabelle_System.create_tmp_path "export" "";
+ val path = Path.expand (Path.explode ("$ISABELLE_EXPORT_TMP/export" ^ serial_string ()));
val _ = File.open_output (fn out => List.app (File.output out) output) path;
- val file_name = Path.implode (Path.expand path);
- in inline_message (#2 function) (tl args @ [(Markup.fileN, file_name)]) end
+ in inline_message (#2 function) (tl args @ [(Markup.fileN, Path.implode path)]) end
else
(case Markup.dest_loading_theory props of
SOME name => writeln ("\floading_theory = " ^ name)
--- a/src/Pure/Tools/build.scala Wed May 16 21:07:12 2018 +0200
+++ b/src/Pure/Tools/build.scala Wed May 16 21:36:59 2018 +0200
@@ -195,6 +195,7 @@
private val graph_file = Isabelle_System.tmp_file("session_graph", "pdf")
isabelle.graphview.Graph_File.write(options, graph_file, deps(name).session_graph_display)
+ private val export_tmp_dir = Isabelle_System.tmp_dir("export")
private val export_consumer = Export.consumer(SQLite.open_database(store.output_database(name)))
private val future_result: Future[Process_Result] =
@@ -222,6 +223,7 @@
val env =
Isabelle_System.settings() +
+ ("ISABELLE_EXPORT_TMP" -> File.standard_path(export_tmp_dir)) +
("ISABELLE_ML_DEBUGGER" -> options.bool("ML_debugger").toString)
def save_heap: String =
@@ -323,6 +325,8 @@
case errs => result.errors(errs)
}
+ Isabelle_System.rm_tree(export_tmp_dir)
+
if (export_result.ok)
Present.finish(progress, store.browser_info, graph_file, info, name)