src/Pure/Tools/server_commands.scala
changeset 76656 a8f452f7c503
parent 76308 fdf823f5b56f
child 76852 2915740fce1f
--- a/src/Pure/Tools/server_commands.scala	Fri Dec 16 17:30:29 2022 +0100
+++ b/src/Pure/Tools/server_commands.scala	Fri Dec 16 17:51:52 2022 +0100
@@ -62,12 +62,12 @@
     def command(
       args: Args,
       progress: Progress = new Progress
-    ) : (JSON.Object.T, Build.Results, Options, Sessions.Base_Info) = {
+    ) : (JSON.Object.T, Build.Results, Options, Sessions.Background) = {
       val options = Options.init(prefs = args.preferences, opts = args.options)
       val dirs = args.dirs.map(Path.explode)
 
-      val base_info =
-        Sessions.base_info(options, args.session, progress = progress, dirs = dirs,
+      val session_background =
+        Sessions.background(options, args.session, progress = progress, dirs = dirs,
           include_sessions = args.include_sessions).check_errors
 
       val results =
@@ -76,11 +76,11 @@
           progress = progress,
           build_heap = true,
           dirs = dirs,
-          infos = base_info.infos,
+          infos = session_background.infos,
           verbose = args.verbose)
 
       val sessions_order =
-        base_info.sessions_structure.imports_topological_order.zipWithIndex.
+        session_background.sessions_structure.imports_topological_order.zipWithIndex.
           toMap.withDefaultValue(-1)
 
       val results_json =
@@ -98,7 +98,7 @@
                 "timing" -> result.timing.json)
             })
 
-      if (results.ok) (results_json, results, options, base_info)
+      if (results.ok) (results_json, results, options, session_background)
       else {
         throw new Server.Error("Session build failed: " + Process_Result.RC.print(results.rc),
           results_json)
@@ -127,11 +127,11 @@
       progress: Progress = new Progress,
       log: Logger = No_Logger
     ) : (JSON.Object.T, (UUID.T, Headless.Session)) = {
-      val (_, _, options, base_info) =
+      val (_, _, options, session_background) =
         try { Session_Build.command(args.build, progress = progress) }
         catch { case exn: Server.Error => error(exn.message) }
 
-      val resources = Headless.Resources(options, base_info, log = log)
+      val resources = Headless.Resources(options, session_background, log = log)
 
       val session = resources.start_session(print_mode = args.print_mode, progress = progress)