# HG changeset patch
# User wenzelm
# Date 1671210768 -3600
# Node ID a8d85b4a588c7a5c57ae129176b79e0799f72089
# Parent  a8f452f7c503db5ed6cfdf90307c18614806ecb1
clarified signature;

diff -r a8f452f7c503 -r a8d85b4a588c src/Pure/ML/ml_process.scala
--- a/src/Pure/ML/ml_process.scala	Fri Dec 16 17:51:52 2022 +0100
+++ b/src/Pure/ML/ml_process.scala	Fri Dec 16 18:12:48 2022 +0100
@@ -13,7 +13,7 @@
 
 object ML_Process {
   def apply(options: Options,
-    background: Sessions.Background,
+    session_background: Sessions.Background,
     store: Sessions.Store,
     logic: String = "",
     raw_ml_system: Boolean = false,
@@ -31,7 +31,7 @@
     val heaps: List[String] =
       if (raw_ml_system) Nil
       else {
-        background.sessions_structure.selection(logic_name).
+        session_background.sessions_structure.selection(logic_name).
           build_requirements(List(logic_name)).
           map(a => File.platform_path(store.the_heap(a)))
       }
@@ -80,8 +80,7 @@
     val eval_init_session = if (raw_ml_system) Nil else List("Resources.init_session_env ()")
     val init_session = Isabelle_System.tmp_file("init_session")
     Isabelle_System.chmod("600", File.path(init_session))
-    val resources = new Resources(background.sessions_structure, background.base)
-    File.write(init_session, resources.init_session_yxml)
+    File.write(init_session, new Resources(session_background).init_session_yxml)
 
     // process
     val eval_process =
@@ -169,11 +168,11 @@
       val more_args = getopts(args)
       if (args.isEmpty || more_args.nonEmpty) getopts.usage()
 
-      val background = Sessions.background(options, logic, dirs = dirs).check_errors
+      val session_background = Sessions.background(options, logic, dirs = dirs).check_errors
       val store = Sessions.store(options)
       val result =
-        ML_Process(options, background, store, logic = logic, args = eval_args, modes = modes)
-          .result(
+        ML_Process(options, session_background, store,
+          logic = logic, args = eval_args, modes = modes).result(
             progress_stdout = Output.writeln(_, stdout = true),
             progress_stderr = Output.writeln(_))
 
diff -r a8f452f7c503 -r a8d85b4a588c src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Fri Dec 16 17:51:52 2022 +0100
+++ b/src/Pure/PIDE/headless.scala	Fri Dec 16 18:12:48 2022 +0100
@@ -445,9 +445,9 @@
   object Resources {
     def apply(
       options: Options,
-      background: Sessions.Background,
+      session_background: Sessions.Background,
       log: Logger = No_Logger
-    ): Resources = new Resources(options, background, log = log)
+    ): Resources = new Resources(options, session_background, log = log)
 
     def make(
       options: Options,
@@ -457,10 +457,10 @@
       progress: Progress = new Progress,
       log: Logger = No_Logger
     ): Resources = {
-      val background =
+      val session_background =
         Sessions.background(options, session_name, dirs = session_dirs,
           include_sessions = include_sessions, progress = progress)
-      apply(options, background, log = log)
+      apply(options, session_background, log = log)
     }
 
     final class Theory private[Headless](
@@ -603,15 +603,13 @@
 
   class Resources private[Headless](
       val options: Options,
-      val session_background: Sessions.Background,
+      session_background: Sessions.Background,
       log: Logger = No_Logger)
-    extends isabelle.Resources(
-      session_background.sessions_structure,
-      session_background.check_errors.base,
-      log = log
-    ) {
+    extends isabelle.Resources(session_background, log = log) {
     resources =>
 
+    session_background.check_errors
+
     val store: Sessions.Store = Sessions.store(options)
 
 
diff -r a8f452f7c503 -r a8d85b4a588c src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Fri Dec 16 17:51:52 2022 +0100
+++ b/src/Pure/PIDE/resources.scala	Fri Dec 16 18:12:48 2022 +0100
@@ -13,7 +13,7 @@
 
 
 object Resources {
-  def bootstrap: Resources = new Resources(Sessions.Structure.empty, Sessions.Base.bootstrap)
+  def bootstrap: Resources = new Resources(Sessions.Background(base = Sessions.Base.bootstrap))
 
   def hidden_node(name: Document.Node.Name): Boolean =
     !name.is_theory || name.theory == Sessions.root_name || File_Format.registry.is_theory(name)
@@ -23,13 +23,15 @@
 }
 
 class Resources(
-  val sessions_structure: Sessions.Structure,
-  val session_base: Sessions.Base,
+  val session_background: Sessions.Background,
   val log: Logger = No_Logger,
   command_timings: List[Properties.T] = Nil
 ) {
   resources =>
 
+  def sessions_structure: Sessions.Structure = session_background.sessions_structure
+  def session_base: Sessions.Base = session_background.base
+  def session_errors: List[String] = session_background.errors
 
   override def toString: String = "Resources(" + session_base.toString + ")"
 
diff -r a8f452f7c503 -r a8d85b4a588c src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Fri Dec 16 17:51:52 2022 +0100
+++ b/src/Pure/Thy/sessions.scala	Fri Dec 16 18:12:48 2022 +0100
@@ -266,7 +266,9 @@
           val info = sessions_structure(session_name)
           try {
             val deps_base = info.deps_base(session_bases)
-            val resources = new Resources(sessions_structure, deps_base)
+            val session_background =
+              Sessions.Background(base = deps_base, sessions_structure = sessions_structure)
+            val resources = new Resources(session_background)
 
             if (verbose || list_files) {
               val groups =
diff -r a8f452f7c503 -r a8d85b4a588c src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Fri Dec 16 17:51:52 2022 +0100
+++ b/src/Pure/Tools/build_job.scala	Fri Dec 16 18:12:48 2022 +0100
@@ -274,8 +274,7 @@
         else Nil
 
       val resources =
-        new Resources(session_background.sessions_structure, session_background.base, log = log,
-          command_timings = command_timings0)
+        new Resources(session_background, log = log, command_timings = command_timings0)
       val session =
         new Session(options, resources) {
           override val cache: Term.Cache = store.cache
diff -r a8f452f7c503 -r a8d85b4a588c src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Fri Dec 16 17:51:52 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Fri Dec 16 18:12:48 2022 +0100
@@ -71,11 +71,7 @@
   val options: Options,
   session_background: Sessions.Background,
   log: Logger = No_Logger)
-extends Resources(
-  session_background.sessions_structure,
-  session_background.check_errors.base,
-  log = log
-) {
+extends Resources(session_background, log = log) {
   resources =>
 
   private val state = Synchronized(VSCode_Resources.State())
diff -r a8f452f7c503 -r a8d85b4a588c src/Tools/jEdit/src/jedit_resources.scala
--- a/src/Tools/jEdit/src/jedit_resources.scala	Fri Dec 16 17:51:52 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Fri Dec 16 18:12:48 2022 +0100
@@ -26,11 +26,8 @@
     new JEdit_Resources(JEdit_Sessions.session_background(options))
 }
 
-class JEdit_Resources private(val session_background: Sessions.Background)
-extends Resources(session_background.sessions_structure, session_background.base) {
-  def session_errors: List[String] = session_background.errors
-
-
+class JEdit_Resources private(session_background: Sessions.Background)
+extends Resources(session_background) {
   /* document node name */
 
   def node_name(path: String): Document.Node.Name =