# HG changeset patch
# User wenzelm
# Date 1585420394 -3600
# Node ID e0a5d60681419202684c28c107e466cbe91551c8
# Parent  fb6953e77000a6c605b452fbf944bd503c3d1880
tuned;

diff -r fb6953e77000 -r e0a5d6068141 src/Pure/System/command_line.scala
--- a/src/Pure/System/command_line.scala	Sat Mar 28 19:11:59 2020 +0100
+++ b/src/Pure/System/command_line.scala	Sat Mar 28 19:33:14 2020 +0100
@@ -36,5 +36,7 @@
   }
 
   def tool0(body: => Unit): Nothing = tool { body; 0 }
+
+  def ML_tool0(body: List[String]): String =
+    "Command_Line.tool0 (fn () => (" + body.mkString("; ") + "));"
 }
-
diff -r fb6953e77000 -r e0a5d6068141 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sat Mar 28 19:11:59 2020 +0100
+++ b/src/Pure/Tools/build.scala	Sat Mar 28 19:33:14 2020 +0100
@@ -239,10 +239,20 @@
 
         val is_pure = Sessions.is_pure(name)
 
-        def save_heap: String =
-          (if (info.theories.isEmpty) "" else "ML_Heap.share_common_data (); ") +
-            "ML_Heap.save_child " +
-            ML_Syntax.print_string_bytes(File.platform_path(store.output_heap(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
+        }
 
         if (pide && !is_pure) {
           val resources = new Resources(sessions_structure, deps(parent))
@@ -269,11 +279,8 @@
           val args_file = Isabelle_System.tmp_file("build")
           File.write(args_file, args_yxml)
 
-          val eval =
-            "Command_Line.tool0 (fn () => (" +
-            "Build.build " + ML_Syntax.print_string_bytes(File.standard_path(args_file)) +
-            (if (is_pure) "; Theory.install_pure (Thy_Info.get_theory Context.PureN)" else "") +
-            (if (do_output) "; " + save_heap else "") + "));"
+          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 process =
             if (is_pure) {