# HG changeset patch
# User wenzelm
# Date 1585421581 -3600
# Node ID 6bce25f9d0ab4bc73381688b9dced7bee71f07ce
# Parent  e0a5d60681419202684c28c107e466cbe91551c8
tuned;

diff -r e0a5d6068141 -r 6bce25f9d0ab src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Sat Mar 28 19:33:14 2020 +0100
+++ b/src/Pure/Tools/build.ML	Sat Mar 28 19:53:01 2020 +0100
@@ -215,6 +215,8 @@
 
     val _ = Resources.finish_session_base ();
     val _ = Par_Exn.release_all [res1, res2];
+    val _ =
+      if name = Context.PureN then Theory.install_pure (Thy_Info.get_theory Context.PureN) else ();
   in () end;
 
 (*command-line tool*)
diff -r e0a5d6068141 -r 6bce25f9d0ab src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sat Mar 28 19:33:14 2020 +0100
+++ b/src/Pure/Tools/build.scala	Sat Mar 28 19:53:01 2020 +0100
@@ -239,20 +239,13 @@
 
         val is_pure = Sessions.is_pure(name)
 
-        val eval_suffix =
-        {
-          val eval_pure =
-            if (is_pure) List("Theory.install_pure (Thy_Info.get_theory Context.PureN)") else Nil
-          val eval_share =
-            if (do_output && info.theories.nonEmpty) List("ML_Heap.share_common_data ()") else Nil
-          val eval_save =
-            if (do_output) {
-              List("ML_Heap.save_child " +
-                ML_Syntax.print_string_bytes(File.platform_path(store.output_heap(name))))
-            }
-            else Nil
-          eval_pure ::: eval_share ::: eval_save
-        }
+        val eval_store =
+          if (!do_output) Nil
+          else {
+            (if (info.theories.nonEmpty) List("ML_Heap.share_common_data ()") else Nil) :::
+            List("ML_Heap.save_child " +
+              ML_Syntax.print_string_bytes(File.platform_path(store.output_heap(name))))
+          }
 
         if (pide && !is_pure) {
           val resources = new Resources(sessions_structure, deps(parent))
@@ -280,7 +273,7 @@
           File.write(args_file, args_yxml)
 
           val eval_build = "Build.build " + ML_Syntax.print_string_bytes(File.standard_path(args_file))
-          val eval = Command_Line.ML_tool0(eval_build :: eval_suffix)
+          val eval = Command_Line.ML_tool0(eval_build :: eval_store)
 
           val process =
             if (is_pure) {