# HG changeset patch
# User wenzelm
# Date 1585686422 -7200
# Node ID ec84f542e4119fcbcd08d3ef3349c2d331d23f93
# Parent  ec14ef6dd09bcaf986852a659fe0f6af96bd7fc6
clarified signature of ML_Process vs. Isabelle_Process: proper support for "isabelle build -P -b";

diff -r ec14ef6dd09b -r ec84f542e411 src/Pure/ML/ml_process.scala
--- a/src/Pure/ML/ml_process.scala	Tue Mar 31 14:40:56 2020 +0200
+++ b/src/Pure/ML/ml_process.scala	Tue Mar 31 22:27:02 2020 +0200
@@ -16,9 +16,11 @@
     sessions_structure: Sessions.Structure,
     store: Sessions.Store,
     logic: String = "",
+    raw_ml_system: Boolean = false,
+    use_prelude: List[String] = Nil,
+    eval_main: String = "",
     args: List[String] = Nil,
     modes: List[String] = Nil,
-    raw_ml_system: Boolean = false,
     cwd: JFile = null,
     env: Map[String, String] = Isabelle_System.settings(),
     redirect: Boolean = false,
@@ -100,9 +102,11 @@
 
     // process
     val eval_process =
-      if (heaps.isEmpty)
-        List("PolyML.print_depth " + ML_Syntax.print_int(options.int("ML_print_depth")))
-      else List("Isabelle_Process.init ()")
+      proper_string(eval_main).getOrElse(
+        if (heaps.isEmpty) {
+          "PolyML.print_depth " + ML_Syntax.print_int(options.int("ML_print_depth"))
+        }
+        else "Isabelle_Process.init ()")
 
     // ISABELLE_TMP
     val isabelle_tmp = Isabelle_System.tmp_dir("process")
@@ -123,8 +127,8 @@
     // bash
     val bash_args =
       ml_runtime_options :::
-      (eval_init ::: eval_modes ::: eval_options ::: eval_session_base ::: eval_process)
-        .flatMap(eval => List("--eval", eval)) ::: args
+      (eval_init ::: eval_modes ::: eval_options ::: eval_session_base).flatMap(List("--eval", _)) :::
+      use_prelude.flatMap(List("--use", _)) ::: List("--eval", eval_process) ::: args
 
     Bash.process(
       "exec " + options.string("ML_process_policy") + """ "$ML_HOME/poly" -q """ +
diff -r ec14ef6dd09b -r ec84f542e411 src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Tue Mar 31 14:40:56 2020 +0200
+++ b/src/Pure/System/isabelle_process.scala	Tue Mar 31 22:27:02 2020 +0200
@@ -18,7 +18,9 @@
     sessions_structure: Sessions.Structure,
     store: Sessions.Store,
     logic: String = "",
-    args: List[String] = Nil,
+    raw_ml_system: Boolean = false,
+    use_prelude: List[String] = Nil,
+    eval_main: String = "",
     modes: List[String] = Nil,
     cwd: JFile = null,
     env: Map[String, String] = Isabelle_System.settings()): Isabelle_Process =
@@ -30,7 +32,9 @@
           options.string.update("system_channel_address", channel.address).
             string.update("system_channel_password", channel.password)
         ML_Process(channel_options, sessions_structure, store,
-          logic = logic, args = args, modes = modes, cwd = cwd, env = env)
+          logic = logic, raw_ml_system = raw_ml_system,
+          use_prelude = use_prelude, eval_main = eval_main,
+          modes = modes, cwd = cwd, env = env)
       }
       catch { case exn @ ERROR(_) => channel.shutdown(); throw exn }
     process.stdin.close
diff -r ec14ef6dd09b -r ec84f542e411 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Tue Mar 31 14:40:56 2020 +0200
+++ b/src/Pure/Tools/build.scala	Tue Mar 31 22:27:02 2020 +0200
@@ -242,23 +242,29 @@
 
         val is_pure = Sessions.is_pure(name)
 
+        val use_prelude = if (is_pure) Thy_Header.ml_roots.map(_._1) else Nil
+
         val eval_store =
-          if (!do_store) Nil
-          else {
+          if (do_store) {
             (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))))
           }
+          else Nil
 
         if (pide && !is_pure) {
-          val resources = new Resources(sessions_structure, deps(parent))
+          val resources = new Resources(sessions_structure, deps(name))
           val session = new Session(options, resources)
           val handler = new Handler(progress, session, name)
           session.init_protocol_handler(handler)
 
+          val eval_main = Command_Line.ML_tool("Isabelle_Process.init ()" :: eval_store)
+
           val process =
             Isabelle_Process(session, options, sessions_structure, store,
-              logic = parent, cwd = info.dir.file, env = env).await_startup
+              logic = parent, raw_ml_system = is_pure,
+              use_prelude = use_prelude, eval_main = eval_main,
+              cwd = info.dir.file, env = env).await_startup
 
           session.protocol_command("build_session", args_yxml)
 
@@ -275,22 +281,15 @@
           val args_file = Isabelle_System.tmp_file("build")
           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_tool(eval_build :: eval_store)
+          val eval_build =
+            "Build.build " + ML_Syntax.print_string_bytes(File.standard_path(args_file))
+          val eval_main = Command_Line.ML_tool(eval_build :: eval_store)
 
           val process =
-            if (is_pure) {
-              ML_Process(options, deps.sessions_structure, store, raw_ml_system = true,
-                args =
-                  (for ((root, _) <- Thy_Header.ml_roots) yield List("--use", root)).flatten :::
-                    List("--eval", eval),
-                cwd = info.dir.file, env = env, cleanup = () => args_file.delete)
-            }
-            else {
-              ML_Process(options, deps.sessions_structure, store, logic = parent,
-                args = List("--eval", eval),
-                cwd = info.dir.file, env = env, cleanup = () => args_file.delete)
-            }
+            ML_Process(options, deps.sessions_structure, store,
+              logic = parent, raw_ml_system = is_pure,
+              use_prelude = use_prelude, eval_main = eval_main,
+              cwd = info.dir.file, env = env, cleanup = () => args_file.delete)
 
           process.result(
             progress_stdout =