# HG changeset patch
# User wenzelm
# Date 1585307000 -3600
# Node ID 8a298184f3f963956f834a576efeacbc92abe155
# Parent  0c6d29145881dd83320353a06571afe8c1cf7e82
clarified signature;

diff -r 0c6d29145881 -r 8a298184f3f9 src/Pure/ML/ml_console.scala
--- a/src/Pure/ML/ml_console.scala	Wed Mar 25 14:00:23 2020 +0000
+++ b/src/Pure/ML/ml_console.scala	Fri Mar 27 12:03:20 2020 +0100
@@ -50,6 +50,8 @@
       if (more_args.nonEmpty) getopts.usage()
 
 
+      val sessions_structure = Sessions.load_structure(options, dirs = dirs)
+
       // build logic
       if (!no_build && !raw_ml_system) {
         val progress = new Console_Progress()
@@ -62,7 +64,7 @@
 
       // process loop
       val process =
-        ML_Process(options, logic = logic, args = List("-i"), dirs = dirs, redirect = true,
+        ML_Process(options, sessions_structure, logic = logic, args = List("-i"), redirect = true,
           modes = if (raw_ml_system) Nil else modes ::: List("ASCII"),
           raw_ml_system = raw_ml_system,
           store = Some(Sessions.store(options)),
diff -r 0c6d29145881 -r 8a298184f3f9 src/Pure/ML/ml_process.scala
--- a/src/Pure/ML/ml_process.scala	Wed Mar 25 14:00:23 2020 +0000
+++ b/src/Pure/ML/ml_process.scala	Fri Mar 27 12:03:20 2020 +0100
@@ -13,29 +13,25 @@
 object ML_Process
 {
   def apply(options: Options,
+    sessions_structure: Sessions.Structure,
     logic: String = "",
     args: List[String] = Nil,
-    dirs: List[Path] = Nil,
     modes: List[String] = Nil,
     raw_ml_system: Boolean = false,
     cwd: JFile = null,
     env: Map[String, String] = Isabelle_System.settings(),
     redirect: Boolean = false,
     cleanup: () => Unit = () => (),
-    sessions_structure: Option[Sessions.Structure] = None,
     session_base: Option[Sessions.Base] = None,
     store: Option[Sessions.Store] = None): Bash.Process =
   {
     val logic_name = Isabelle_System.default_logic(logic)
     val _store = store.getOrElse(Sessions.store(options))
 
-    val sessions_structure1 =
-      sessions_structure.getOrElse(Sessions.load_structure(options, dirs = dirs))
-
     val heaps: List[String] =
       if (raw_ml_system) Nil
       else {
-        sessions_structure1.selection(Sessions.Selection.session(logic_name)).
+        sessions_structure.selection(Sessions.Selection.session(logic_name)).
           build_requirements(List(logic_name)).
           map(a => File.platform_path(_store.the_heap(a)))
       }
@@ -96,8 +92,8 @@
               ML_Syntax.print_pair(ML_Syntax.print_string_bytes, ML_Syntax.print_properties))(list)
 
           List("Resources.init_session_base" +
-            " {session_positions = " + print_sessions(sessions_structure1.session_positions) +
-            ", session_directories = " + print_table(sessions_structure1.dest_session_directories) +
+            " {session_positions = " + print_sessions(sessions_structure.session_positions) +
+            ", session_directories = " + print_table(sessions_structure.dest_session_directories) +
             ", docs = " + print_list(base.doc_names) +
             ", global_theories = " + print_table(base.global_theories.toList) +
             ", loaded_theories = " + print_list(base.loaded_theories.keys) + "}")
@@ -182,8 +178,11 @@
     val more_args = getopts(args)
     if (args.isEmpty || more_args.nonEmpty) getopts.usage()
 
-    val rc = ML_Process(options, logic = logic, args = eval_args, dirs = dirs, modes = modes).
-      result().print_stdout.rc
+    val sessions_structure = Sessions.load_structure(options, dirs = dirs)
+
+    val rc =
+      ML_Process(options, sessions_structure, logic = logic, args = eval_args, modes = modes)
+        .result().print_stdout.rc
     sys.exit(rc)
   })
 }
diff -r 0c6d29145881 -r 8a298184f3f9 src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Wed Mar 25 14:00:23 2020 +0000
+++ b/src/Pure/PIDE/headless.scala	Fri Mar 27 12:03:20 2020 +0100
@@ -584,9 +584,11 @@
         }
       session.phase_changed += session_phase
 
+      val sessions_structure = Sessions.load_structure(options, dirs = session_base_info.dirs)
+
       progress.echo("Starting session " + session_base_info.session + " ...")
-      Isabelle_Process.start(session, options,
-        logic = session_base_info.session, dirs = session_base_info.dirs, modes = print_mode)
+      Isabelle_Process.start(session, options, sessions_structure,
+        logic = session_base_info.session, modes = print_mode)
 
       session_error.join match {
         case "" => session
diff -r 0c6d29145881 -r 8a298184f3f9 src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Wed Mar 25 14:00:23 2020 +0000
+++ b/src/Pure/System/isabelle_process.scala	Fri Mar 27 12:03:20 2020 +0100
@@ -12,15 +12,15 @@
 
 object Isabelle_Process
 {
-  def start(session: Session,
+  def start(
+    session: Session,
     options: Options,
+    sessions_structure: Sessions.Structure,
     logic: String = "",
     args: List[String] = Nil,
-    dirs: List[Path] = Nil,
     modes: List[String] = Nil,
     cwd: JFile = null,
     env: Map[String, String] = Isabelle_System.settings(),
-    sessions_structure: Option[Sessions.Structure] = None,
     store: Option[Sessions.Store] = None,
     phase_changed: Session.Phase => Unit = null)
   {
@@ -28,22 +28,20 @@
       session.phase_changed += Session.Consumer("Isabelle_Process")(phase_changed)
 
     session.start(receiver =>
-      Isabelle_Process(options, logic = logic, args = args, dirs = dirs, modes = modes,
-        cwd = cwd, env = env, receiver = receiver, xml_cache = session.xml_cache,
-        sessions_structure = sessions_structure, store = store))
+      Isabelle_Process(options, sessions_structure, logic = logic, args = args, modes = modes,
+        cwd = cwd, env = env, receiver = receiver, xml_cache = session.xml_cache, store = store))
   }
 
   def apply(
     options: Options,
+    sessions_structure: Sessions.Structure,
     logic: String = "",
     args: List[String] = Nil,
-    dirs: List[Path] = Nil,
     modes: List[String] = Nil,
     cwd: JFile = null,
     env: Map[String, String] = Isabelle_System.settings(),
     receiver: Prover.Receiver = (msg: Prover.Message) => Output.writeln(msg.toString, stdout = true),
     xml_cache: XML.Cache = XML.make_cache(),
-    sessions_structure: Option[Sessions.Structure] = None,
     store: Option[Sessions.Store] = None): Prover =
   {
     val channel = System_Channel()
@@ -52,8 +50,9 @@
         val channel_options =
           options.string.update("system_channel_address", channel.address).
             string.update("system_channel_password", channel.password)
-        ML_Process(channel_options, logic = logic, args = args, dirs = dirs, modes = modes,
-            cwd = cwd, env = env, sessions_structure = sessions_structure, store = store)
+        ML_Process(
+          channel_options, sessions_structure, logic = logic, args = args, modes = modes,
+          cwd = cwd, env = env, store = store)
       }
       catch { case exn @ ERROR(_) => channel.shutdown(); throw exn }
     process.stdin.close
diff -r 0c6d29145881 -r 8a298184f3f9 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Mar 25 14:00:23 2020 +0000
+++ b/src/Pure/Tools/build.scala	Fri Mar 27 12:03:20 2020 +0100
@@ -250,8 +250,8 @@
 
           val session_result = Future.promise[Process_Result]
 
-          Isabelle_Process.start(session, options, logic = parent, cwd = info.dir.file, env = env,
-            sessions_structure = Some(sessions_structure), store = Some(store),
+          Isabelle_Process.start(session, options, sessions_structure,
+            logic = parent, cwd = info.dir.file, env = env, store = Some(store),
             phase_changed =
             {
               case Session.Ready => session.protocol_command("build_session", args_yxml)
@@ -280,16 +280,16 @@
 
           val process =
             if (Sessions.is_pure(name)) {
-              ML_Process(options, raw_ml_system = true, cwd = info.dir.file,
+              ML_Process(options, deps.sessions_structure, raw_ml_system = true,
+                cwd = info.dir.file, env = env, store = Some(store),
                 args =
                   (for ((root, _) <- Thy_Header.ml_roots) yield List("--use", root)).flatten :::
                   List("--eval", eval),
-                env = env, sessions_structure = Some(deps.sessions_structure), store = Some(store),
                 cleanup = () => args_file.delete)
             }
             else {
-              ML_Process(options, parent, List("--eval", eval), cwd = info.dir.file,
-                env = env, sessions_structure = Some(deps.sessions_structure), store = Some(store),
+              ML_Process(options, deps.sessions_structure, parent, List("--eval", eval),
+                cwd = info.dir.file, env = env, store = Some(store),
                 cleanup = () => args_file.delete)
             }
 
diff -r 0c6d29145881 -r 8a298184f3f9 src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Wed Mar 25 14:00:23 2020 +0000
+++ b/src/Tools/VSCode/src/server.scala	Fri Mar 27 12:03:20 2020 +0100
@@ -318,8 +318,8 @@
         }
       session.phase_changed += session_phase
 
-      Isabelle_Process.start(session, options, modes = modes,
-        sessions_structure = Some(base_info.sessions_structure), logic = base_info.session)
+      Isabelle_Process.start(
+        session, options, base_info.sessions_structure, modes = modes, logic = base_info.session)
     }
   }
 
diff -r 0c6d29145881 -r 8a298184f3f9 src/Tools/jEdit/src/jedit_sessions.scala
--- a/src/Tools/jEdit/src/jedit_sessions.scala	Wed Mar 25 14:00:23 2020 +0000
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Fri Mar 27 12:03:20 2020 +0100
@@ -138,7 +138,7 @@
     val options = session_options(options0)
 
     Isabelle_Process.start(PIDE.session, options,
-      sessions_structure = Some(PIDE.resources.session_base_info.sessions_structure),
+      PIDE.resources.session_base_info.sessions_structure,
       logic = PIDE.resources.session_name,
       store = Some(Sessions.store(options)),
       modes =