avoid race condition wrt. ISABELLE_TMP, which is removed in Bash.cleanup() before Bash.result(progress_stdout);
authorwenzelm
Wed May 16 21:36:59 2018 +0200 (5 months ago)
changeset 681986710167e17af
parent 68197 7857817403e4
child 68199 f551dd2178ab
avoid race condition wrt. ISABELLE_TMP, which is removed in Bash.cleanup() before Bash.result(progress_stdout);
src/Pure/Tools/build.ML
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/Tools/build.ML	Wed May 16 21:07:12 2018 +0200
     1.2 +++ b/src/Pure/Tools/build.ML	Wed May 16 21:36:59 2018 +0200
     1.3 @@ -98,10 +98,9 @@
     1.4          not (null args) andalso #1 (hd args) = Markup.idN
     1.5        then
     1.6          let
     1.7 -          val path = Isabelle_System.create_tmp_path "export" "";
     1.8 +          val path = Path.expand (Path.explode ("$ISABELLE_EXPORT_TMP/export" ^ serial_string ()));
     1.9            val _ = File.open_output (fn out => List.app (File.output out) output) path;
    1.10 -          val file_name = Path.implode (Path.expand path);
    1.11 -        in inline_message (#2 function) (tl args @ [(Markup.fileN, file_name)]) end
    1.12 +        in inline_message (#2 function) (tl args @ [(Markup.fileN, Path.implode path)]) end
    1.13        else
    1.14          (case Markup.dest_loading_theory props of
    1.15            SOME name => writeln ("\floading_theory = " ^ name)
     2.1 --- a/src/Pure/Tools/build.scala	Wed May 16 21:07:12 2018 +0200
     2.2 +++ b/src/Pure/Tools/build.scala	Wed May 16 21:36:59 2018 +0200
     2.3 @@ -195,6 +195,7 @@
     2.4      private val graph_file = Isabelle_System.tmp_file("session_graph", "pdf")
     2.5      isabelle.graphview.Graph_File.write(options, graph_file, deps(name).session_graph_display)
     2.6  
     2.7 +    private val export_tmp_dir = Isabelle_System.tmp_dir("export")
     2.8      private val export_consumer = Export.consumer(SQLite.open_database(store.output_database(name)))
     2.9  
    2.10      private val future_result: Future[Process_Result] =
    2.11 @@ -222,6 +223,7 @@
    2.12  
    2.13          val env =
    2.14            Isabelle_System.settings() +
    2.15 +            ("ISABELLE_EXPORT_TMP" -> File.standard_path(export_tmp_dir)) +
    2.16              ("ISABELLE_ML_DEBUGGER" -> options.bool("ML_debugger").toString)
    2.17  
    2.18          def save_heap: String =
    2.19 @@ -323,6 +325,8 @@
    2.20            case errs => result.errors(errs)
    2.21          }
    2.22  
    2.23 +      Isabelle_System.rm_tree(export_tmp_dir)
    2.24 +
    2.25        if (export_result.ok)
    2.26          Present.finish(progress, store.browser_info, graph_file, info, name)
    2.27