clarified signature: allow to provide session_heaps by different means, e.g. from tmp directory or alternative session structure;

--- a/src/Pure/ML/ml_console.scala	Tue Feb 28 17:16:50 2023 +0100
+++ b/src/Pure/ML/ml_console.scala	Tue Feb 28 17:42:13 2023 +0100
@@ -71,12 +71,14 @@
             options, logic, dirs = dirs, include_sessions = include_sessions).check_errors
         }
 
+      val session_heaps =
+        if (raw_ml_system) Nil
+        else ML_Process.session_heaps(store, session_background, logic = logic)
+
       // process loop
       val process =
-        ML_Process(store, options, session_background,
-          logic = logic, args = List("-i"), redirect = true,
-          modes = if (raw_ml_system) Nil else modes ::: List("ASCII"),
-          raw_ml_system = raw_ml_system)
+        ML_Process(options, session_background, session_heaps, args = List("-i"), redirect = true,
+          modes = if (raw_ml_system) Nil else modes ::: List("ASCII"))
 
       POSIX_Interrupt.handler { process.interrupt() } {
         new TTY_Loop(process.stdin, process.stdout).join()

--- a/src/Pure/ML/ml_process.scala	Tue Feb 28 17:16:50 2023 +0100
+++ b/src/Pure/ML/ml_process.scala	Tue Feb 28 17:42:13 2023 +0100
@@ -12,12 +12,22 @@
 
 
 object ML_Process {
+  def session_heaps(
+    store: Sessions.Store,
+    session_background: Sessions.Background,
+    logic: String = ""
+  ): List[Path] = {
+    val logic_name = Isabelle_System.default_logic(logic)
+
+    session_background.sessions_structure.selection(logic_name).
+      build_requirements(List(logic_name)).
+      map(store.the_heap)
+  }
+
   def apply(
-    store: Sessions.Store,
     options: Options,
     session_background: Sessions.Background,
-    logic: String = "",
-    raw_ml_system: Boolean = false,
+    session_heaps: List[Path],
     use_prelude: List[String] = Nil,
     eval_main: String = "",
     args: List[String] = Nil,
@@ -27,18 +37,8 @@
     redirect: Boolean = false,
     cleanup: () => Unit = () => ()
   ): Bash.Process = {
-    val logic_name = Isabelle_System.default_logic(logic)
-
-    val heaps: List[String] =
-      if (raw_ml_system) Nil
-      else {
-        session_background.sessions_structure.selection(logic_name).
-          build_requirements(List(logic_name)).
-          map(a => File.platform_path(store.the_heap(a)))
-      }
-
     val eval_init =
-      if (heaps.isEmpty) {
+      if (session_heaps.isEmpty) {
         List(
           """
           fun chapter (_: string) = ();
@@ -61,7 +61,9 @@
       else {
         List(
           "(PolyML.SaveState.loadHierarchy " +
-            ML_Syntax.print_list(ML_Syntax.print_string_bytes)(heaps) + "; PolyML.print_depth 0)")
+            ML_Syntax.print_list(
+              ML_Syntax.print_string_bytes)(session_heaps.map(File.platform_path)) +
+          "; PolyML.print_depth 0)")
       }
 
     val eval_modes =
@@ -70,13 +72,13 @@
 
 
     // options
-    val eval_options = if (heaps.isEmpty) Nil else List("Options.load_default ()")
+    val eval_options = if (session_heaps.isEmpty) Nil else List("Options.load_default ()")
     val isabelle_process_options = Isabelle_System.tmp_file("options")
     Isabelle_System.chmod("600", File.path(isabelle_process_options))
     File.write(isabelle_process_options, YXML.string_of_body(options.encode))
 
     // session resources
-    val eval_init_session = if (raw_ml_system) Nil else List("Resources.init_session_env ()")
+    val eval_init_session = if (session_heaps.isEmpty) Nil else List("Resources.init_session_env ()")
     val init_session = Isabelle_System.tmp_file("init_session")
     Isabelle_System.chmod("600", File.path(init_session))
     File.write(init_session, new Resources(session_background).init_session_yxml)
@@ -84,7 +86,7 @@
     // process
     val eval_process =
       proper_string(eval_main).getOrElse(
-        if (heaps.isEmpty) {
+        if (session_heaps.isEmpty) {
           "PolyML.print_depth " + ML_Syntax.print_int(options.int("ML_print_depth"))
         }
         else "Isabelle_Process.init ()")
@@ -169,9 +171,10 @@
 
       val store = Sessions.store(options)
       val session_background = Sessions.background(options, logic, dirs = dirs).check_errors
+      val session_heaps = ML_Process.session_heaps(store, session_background, logic = logic)
       val result =
-        ML_Process(store, options, session_background,
-          logic = logic, args = eval_args, modes = modes).result(
+        ML_Process(options, session_background, session_heaps, args = eval_args, modes = modes)
+          .result(
             progress_stdout = Output.writeln(_, stdout = true),
             progress_stderr = Output.writeln(_))
 

--- a/src/Pure/PIDE/headless.scala	Tue Feb 28 17:16:50 2023 +0100
+++ b/src/Pure/PIDE/headless.scala	Tue Feb 28 17:42:13 2023 +0100
@@ -619,10 +619,11 @@
     ): Session = {
       val session_name = session_background.session_name
       val session = new Session(session_name, options, resources)
+      val session_heaps = ML_Process.session_heaps(store, session_background, logic = session_name)
 
       progress.echo("Starting session " + session_name + " ...")
-      Isabelle_Process.start(store, options, session, session_background,
-        logic = session_name, modes = print_mode).await_startup()
+      Isabelle_Process.start(
+        options, session, session_background, session_heaps, modes = print_mode).await_startup()
 
       session
     }

--- a/src/Pure/System/isabelle_process.scala	Tue Feb 28 17:16:50 2023 +0100
+++ b/src/Pure/System/isabelle_process.scala	Tue Feb 28 17:42:13 2023 +0100
@@ -13,12 +13,10 @@
 
 object Isabelle_Process {
   def start(
-    store: Sessions.Store,
     options: Options,
     session: Session,
     session_background: Sessions.Background,
-    logic: String = "",
-    raw_ml_system: Boolean = false,
+    session_heaps: List[Path],
     use_prelude: List[String] = Nil,
     eval_main: String = "",
     modes: List[String] = Nil,
@@ -32,8 +30,7 @@
           options.
             string.update("system_channel_address", channel.address).
             string.update("system_channel_password", channel.password)
-        ML_Process(store, ml_options, session_background,
-          logic = logic, raw_ml_system = raw_ml_system,
+        ML_Process(ml_options, session_background, session_heaps,
           use_prelude = use_prelude, eval_main = eval_main,
           modes = modes, cwd = cwd, env = env)
       }

--- a/src/Pure/Tools/build_job.scala	Tue Feb 28 17:16:50 2023 +0100
+++ b/src/Pure/Tools/build_job.scala	Tue Feb 28 17:42:13 2023 +0100
@@ -43,6 +43,7 @@
     progress: Progress,
     verbose: Boolean,
     session_background: Sessions.Background,
+    session_heaps: List[Path],
     store: Sessions.Store,
     do_store: Boolean,
     resources: Resources,
@@ -62,15 +63,11 @@
 
     private lazy val future_result: Future[Process_Result] =
       Future.thread("build", uninterruptible = true) {
-        val parent = info.parent.getOrElse("")
-
         val env =
           Isabelle_System.settings(
             List("ISABELLE_ML_DEBUGGER" -> options.bool("ML_debugger").toString))
 
-        val is_pure = Sessions.is_pure(session_name)
-
-        val use_prelude = if (is_pure) Thy_Header.ml_roots.map(_._1) else Nil
+        val use_prelude = if (session_heaps.isEmpty) Thy_Header.ml_roots.map(_._1) else Nil
 
         val eval_store =
           if (do_store) {
@@ -268,11 +265,10 @@
 
         val eval_main = Command_Line.ML_tool("Isabelle_Process.init_build ()" :: eval_store)
 
-        val process =
-          Isabelle_Process.start(store, options, session, session_background,
-            logic = parent, raw_ml_system = is_pure,
-            use_prelude = use_prelude, eval_main = eval_main,
-            cwd = info.dir.file, env = env)
+        val process = {
+          Isabelle_Process.start(options, session, session_background, session_heaps,
+            use_prelude = use_prelude, eval_main = eval_main, cwd = info.dir.file, env = env)
+        }
 
         val build_errors =
           Isabelle_Thread.interrupt_handler(_ => process.terminate()) {

--- a/src/Pure/Tools/build_process.scala	Tue Feb 28 17:16:50 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Tue Feb 28 17:42:13 2023 +0100
@@ -586,6 +586,12 @@
         store.init_session_info(_, session_name))
 
       val session_background = build_deps.background(session_name)
+      val session_heaps =
+        session_background.info.parent match {
+          case None => Nil
+          case Some(logic) => ML_Process.session_heaps(store, session_background, logic = logic)
+        }
+
       val resources =
         new Resources(session_background, log = log,
           command_timings = build_context(session_name).old_command_timings)
@@ -595,9 +601,9 @@
           val (numa_node, state1) = _state.numa_next(build_context.numa_nodes)
           val node_info = Build_Job.Node_Info(build_context.hostname, numa_node)
           val job =
-            new Build_Job.Build_Session(progress, verbose, session_background, store, do_store,
-              resources, build_context.session_setup, build_deps.sources_shasum(session_name),
-              input_heaps, node_info)
+            new Build_Job.Build_Session(progress, verbose, session_background, session_heaps,
+              store, do_store, resources, build_context.session_setup,
+              build_deps.sources_shasum(session_name), input_heaps, node_info)
           _state = state1.add_running(session_name, job)
           job
         }

--- a/src/Tools/VSCode/src/language_server.scala	Tue Feb 28 17:16:50 2023 +0100
+++ b/src/Tools/VSCode/src/language_server.scala	Tue Feb 28 17:42:13 2023 +0100
@@ -297,6 +297,8 @@
 
     for ((session_background, session) <- try_session) {
       val store = Sessions.store(options)
+      val session_heaps =
+        ML_Process.session_heaps(store, session_background, logic = session_background.session_name)
 
       session_.change(_ => Some(session))
 
@@ -306,8 +308,8 @@
       dynamic_output.init()
 
       try {
-        Isabelle_Process.start(store, options, session, session_background,
-          modes = modes, logic = session_background.session_name).await_startup()
+        Isabelle_Process.start(
+          options, session, session_background, session_heaps, modes = modes).await_startup()
         reply_ok(
           "Welcome to Isabelle/" + session_background.session_name +
           Isabelle_System.isabelle_heading())

--- a/src/Tools/jEdit/src/jedit_sessions.scala	Tue Feb 28 17:16:50 2023 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Tue Feb 28 17:42:13 2023 +0100
@@ -162,11 +162,12 @@
     val session = PIDE.session
     val session_background = PIDE.resources.session_background
     val store = sessions_store(options = options)
+    val session_heaps =
+      ML_Process.session_heaps(store, session_background, logic = session_background.session_name)
 
     session.phase_changed += PIDE.plugin.session_phase_changed
 
-    Isabelle_Process.start(store, store.options, session, session_background,
-      logic = session_background.session_name,
+    Isabelle_Process.start(store.options, session, session_background, session_heaps,
       modes =
         (space_explode(',', store.options.string("jedit_print_mode")) :::
          space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).reverse)