src/Pure/ML/ml_process.scala
changeset 76657 a8d85b4a588c
parent 76656 a8f452f7c503
child 76729 b045b40a65cc
--- 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(_))