clarified names;

--- a/src/Pure/Admin/build_doc.scala	Fri Dec 16 17:30:29 2022 +0100
+++ b/src/Pure/Admin/build_doc.scala	Fri Dec 16 17:51:52 2022 +0100
@@ -54,7 +54,7 @@
             progress.expose_interrupt()
             progress.echo("Documentation " + quote(doc) + " ...")
 
-            using(Export.open_session_context(build_results.store, deps.base_info(session))) {
+            using(Export.open_session_context(build_results.store, deps.background(session))) {
               session_context =>
                 Document_Build.build_documents(
                   Document_Build.context(session_context),

--- a/src/Pure/ML/ml_console.scala	Fri Dec 16 17:30:29 2022 +0100
+++ b/src/Pure/ML/ml_console.scala	Fri Dec 16 17:51:52 2022 +0100
@@ -60,20 +60,20 @@
         if (rc != Process_Result.RC.ok) sys.exit(rc)
       }
 
-      val base_info =
+      val background =
         if (raw_ml_system) {
-          Sessions.Base_Info(
+          Sessions.Background(
             base = Sessions.Base.bootstrap,
             sessions_structure = Sessions.load_structure(options, dirs = dirs))
         }
         else {
-          Sessions.base_info(
+          Sessions.background(
             options, logic, dirs = dirs, include_sessions = include_sessions).check_errors
         }
 
       // process loop
       val process =
-        ML_Process(options, base_info, store,
+        ML_Process(options, background, store,
           logic = logic, args = List("-i"), redirect = true,
           modes = if (raw_ml_system) Nil else modes ::: List("ASCII"),
           raw_ml_system = raw_ml_system)

--- a/src/Pure/ML/ml_process.scala	Fri Dec 16 17:30:29 2022 +0100
+++ b/src/Pure/ML/ml_process.scala	Fri Dec 16 17:51:52 2022 +0100
@@ -13,7 +13,7 @@
 
 object ML_Process {
   def apply(options: Options,
-    base_info: Sessions.Base_Info,
+    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 {
-        base_info.sessions_structure.selection(logic_name).
+        background.sessions_structure.selection(logic_name).
           build_requirements(List(logic_name)).
           map(a => File.platform_path(store.the_heap(a)))
       }
@@ -80,7 +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(base_info.sessions_structure, base_info.base)
+    val resources = new Resources(background.sessions_structure, background.base)
     File.write(init_session, resources.init_session_yxml)
 
     // process
@@ -169,10 +169,10 @@
       val more_args = getopts(args)
       if (args.isEmpty || more_args.nonEmpty) getopts.usage()
 
-      val base_info = Sessions.base_info(options, logic, dirs = dirs).check_errors
+      val background = Sessions.background(options, logic, dirs = dirs).check_errors
       val store = Sessions.store(options)
       val result =
-        ML_Process(options, base_info, store, logic = logic, args = eval_args, modes = modes)
+        ML_Process(options, background, store, logic = logic, args = eval_args, modes = modes)
           .result(
             progress_stdout = Output.writeln(_, stdout = true),
             progress_stderr = Output.writeln(_))

--- a/src/Pure/PIDE/document_info.scala	Fri Dec 16 17:30:29 2022 +0100
+++ b/src/Pure/PIDE/document_info.scala	Fri Dec 16 17:51:52 2022 +0100
@@ -113,7 +113,7 @@
     def read_session(session_name: String): Document_Info.Session = {
       val static_theories = deps(session_name).used_theories.map(_._1.theory)
       val (thys, build_uuid) = {
-        using(database_context.open_session(deps.base_info(session_name))) { session_context =>
+        using(database_context.open_session(deps.background(session_name))) { session_context =>
           val thys =
             for {
               theory_name <- static_theories

--- a/src/Pure/PIDE/headless.scala	Fri Dec 16 17:30:29 2022 +0100
+++ b/src/Pure/PIDE/headless.scala	Fri Dec 16 17:51:52 2022 +0100
@@ -443,8 +443,11 @@
   /** resources **/
 
   object Resources {
-    def apply(options: Options, base_info: Sessions.Base_Info, log: Logger = No_Logger): Resources =
-      new Resources(options, base_info, log = log)
+    def apply(
+      options: Options,
+      background: Sessions.Background,
+      log: Logger = No_Logger
+    ): Resources = new Resources(options, background, log = log)
 
     def make(
       options: Options,
@@ -454,10 +457,10 @@
       progress: Progress = new Progress,
       log: Logger = No_Logger
     ): Resources = {
-      val base_info =
-        Sessions.base_info(options, session_name, dirs = session_dirs,
+      val background =
+        Sessions.background(options, session_name, dirs = session_dirs,
           include_sessions = include_sessions, progress = progress)
-      apply(options, base_info, log = log)
+      apply(options, background, log = log)
     }
 
     final class Theory private[Headless](
@@ -600,11 +603,11 @@
 
   class Resources private[Headless](
       val options: Options,
-      val session_base_info: Sessions.Base_Info,
+      val session_background: Sessions.Background,
       log: Logger = No_Logger)
     extends isabelle.Resources(
-      session_base_info.sessions_structure,
-      session_base_info.check_errors.base,
+      session_background.sessions_structure,
+      session_background.check_errors.base,
       log = log
     ) {
     resources =>
@@ -618,11 +621,11 @@
       print_mode: List[String] = Nil,
       progress: Progress = new Progress
     ): Session = {
-      val session_name = session_base_info.session_name
+      val session_name = session_background.session_name
       val session = new Session(session_name, options, resources)
 
       progress.echo("Starting session " + session_name + " ...")
-      Isabelle_Process.start(session, options, session_base_info, store,
+      Isabelle_Process.start(session, options, session_background, store,
         logic = session_name, modes = print_mode).await_startup()
 
       session

--- a/src/Pure/System/isabelle_process.scala	Fri Dec 16 17:30:29 2022 +0100
+++ b/src/Pure/System/isabelle_process.scala	Fri Dec 16 17:51:52 2022 +0100
@@ -15,7 +15,7 @@
   def start(
     session: Session,
     options: Options,
-    base_info: Sessions.Base_Info,
+    session_background: Sessions.Background,
     store: Sessions.Store,
     logic: String = "",
     raw_ml_system: Boolean = false,
@@ -31,7 +31,7 @@
         val channel_options =
           options.string.update("system_channel_address", channel.address).
             string.update("system_channel_password", channel.password)
-        ML_Process(channel_options, base_info, store,
+        ML_Process(channel_options, session_background, store,
           logic = logic, raw_ml_system = raw_ml_system,
           use_prelude = use_prelude, eval_main = eval_main,
           modes = modes, cwd = cwd, env = env)

--- a/src/Pure/Thy/browser_info.scala	Fri Dec 16 17:30:29 2022 +0100
+++ b/src/Pure/Thy/browser_info.scala	Fri Dec 16 17:51:52 2022 +0100
@@ -694,7 +694,7 @@
       context1.update_root()
 
       Par_List.map({ (session: String) =>
-        using(database_context.open_session(deps.base_info(session))) { session_context =>
+        using(database_context.open_session(deps.background(session))) { session_context =>
           build_session(context1, session_context, progress = progress, verbose = verbose)
         }
       }, sessions1)

--- a/src/Pure/Thy/document_build.scala	Fri Dec 16 17:30:29 2022 +0100
+++ b/src/Pure/Thy/document_build.scala	Fri Dec 16 17:51:52 2022 +0100
@@ -511,13 +511,13 @@
             Sessions.load_structure(options + "document=pdf", dirs = dirs).
               selection_deps(Sessions.Selection.session(session))
 
-          val session_base_info = deps.base_info(session)
+          val session_background = deps.background(session)
 
           if (output_sources.isEmpty && output_pdf.isEmpty) {
             progress.echo_warning("No output directory")
           }
 
-          using(Export.open_session_context(build_results.store, session_base_info)) {
+          using(Export.open_session_context(build_results.store, session_background)) {
             session_context =>
               build_documents(
                 context(session_context, progress = progress),

--- a/src/Pure/Thy/export.scala	Fri Dec 16 17:30:29 2022 +0100
+++ b/src/Pure/Thy/export.scala	Fri Dec 16 17:51:52 2022 +0100
@@ -251,11 +251,11 @@
 
   def open_session_context(
     store: Sessions.Store,
-    session_base_info: Sessions.Base_Info,
+    session_background: Sessions.Background,
     document_snapshot: Option[Document.Snapshot] = None
   ): Session_Context = {
     open_database_context(store).open_session(
-      session_base_info, document_snapshot = document_snapshot, close_database_context = true)
+      session_background, document_snapshot = document_snapshot, close_database_context = true)
   }
 
   class Database_Context private[Export](
@@ -287,15 +287,15 @@
       }
 
     def open_session0(session: String, close_database_context: Boolean = false): Session_Context =
-      open_session(Sessions.base_info0(session), close_database_context = close_database_context)
+      open_session(Sessions.background0(session), close_database_context = close_database_context)
 
     def open_session(
-      session_base_info: Sessions.Base_Info,
+      session_background: Sessions.Background,
       document_snapshot: Option[Document.Snapshot] = None,
       close_database_context: Boolean = false
     ): Session_Context = {
-      val session_name = session_base_info.check_errors.session_name
-      val session_hierarchy = session_base_info.sessions_structure.build_hierarchy(session_name)
+      val session_name = session_background.check_errors.session_name
+      val session_hierarchy = session_background.sessions_structure.build_hierarchy(session_name)
       val session_databases =
         database_server match {
           case Some(db) => session_hierarchy.map(name => new Session_Database(name, db))
@@ -312,7 +312,8 @@
                 }
             }
         }
-      new Session_Context(database_context, session_base_info, session_databases, document_snapshot) {
+      new Session_Context(
+          database_context, session_background, session_databases, document_snapshot) {
         override def close(): Unit = {
           session_databases.foreach(_.close())
           if (close_database_context) database_context.close()
@@ -331,7 +332,7 @@
 
   class Session_Context private[Export](
     val database_context: Database_Context,
-    session_base_info: Sessions.Base_Info,
+    session_background: Sessions.Background,
     db_hierarchy: List[Session_Database],
     document_snapshot: Option[Document.Snapshot]
   ) extends AutoCloseable {
@@ -341,9 +342,9 @@
 
     def cache: Term.Cache = database_context.cache
 
-    def sessions_structure: Sessions.Structure = session_base_info.sessions_structure
+    def sessions_structure: Sessions.Structure = session_background.sessions_structure
 
-    def session_base: Sessions.Base = session_base_info.base
+    def session_base: Sessions.Base = session_background.base
 
     def session_name: String =
       if (document_snapshot.isDefined) Sessions.DRAFT

--- a/src/Pure/Thy/sessions.scala	Fri Dec 16 17:30:29 2022 +0100
+++ b/src/Pure/Thy/sessions.scala	Fri Dec 16 17:51:52 2022 +0100
@@ -101,7 +101,7 @@
       nodes(name).syntax orElse loaded_theory_syntax(name) getOrElse overall_syntax
   }
 
-  sealed case class Base_Info(
+  sealed case class Background(
     base: Base,
     sessions_structure: Structure = Structure.empty,
     errors: List[String] = Nil,
@@ -109,22 +109,22 @@
   ) {
     def session_name: String = base.session_name
 
-    def check_errors: Base_Info =
+    def check_errors: Background =
       if (errors.isEmpty) this
       else error(cat_lines(errors))
   }
 
-  def base_info0(session: String): Base_Info =
-    Base_Info(Base(session_name = session))
+  def background0(session: String): Background =
+    Background(Base(session_name = session))
 
-  def base_info(options: Options,
+  def background(options: Options,
     session: String,
     progress: Progress = new Progress,
     dirs: List[Path] = Nil,
     include_sessions: List[String] = Nil,
     session_ancestor: Option[String] = None,
     session_requirements: Boolean = false
-  ): Base_Info = {
+  ): Background = {
     val full_sessions = load_structure(options, dirs = dirs)
 
     val selected_sessions =
@@ -194,7 +194,7 @@
 
     val deps1 = Sessions.deps(selected_sessions1, progress = progress)
 
-    Base_Info(deps1(session1), sessions_structure = full_sessions1,
+    Background(deps1(session1), sessions_structure = full_sessions1,
       errors = deps1.errors, infos = infos1)
   }
 
@@ -202,8 +202,8 @@
   /* source dependencies */
 
   sealed case class Deps(sessions_structure: Structure, session_bases: Map[String, Base]) {
-    def base_info(session: String): Base_Info =
-      Base_Info(base = apply(session), sessions_structure = sessions_structure, errors = errors)
+    def background(session: String): Background =
+      Background(base = apply(session), sessions_structure = sessions_structure, errors = errors)
 
     def is_empty: Boolean = session_bases.keysIterator.forall(_.isEmpty)
     def apply(name: String): Base = session_bases(name)

--- a/src/Pure/Tools/build_job.scala	Fri Dec 16 17:30:29 2022 +0100
+++ b/src/Pure/Tools/build_job.scala	Fri Dec 16 17:51:52 2022 +0100
@@ -249,7 +249,7 @@
 ) {
   val options: Options = NUMA.policy_options(info.options, numa_node)
 
-  private val base_info = deps.base_info(session_name)
+  private val session_background = deps.background(session_name)
 
   private val future_result: Future[Process_Result] =
     Future.thread("build", uninterruptible = true) {
@@ -274,7 +274,7 @@
         else Nil
 
       val resources =
-        new Resources(base_info.sessions_structure, base_info.base, log = log,
+        new Resources(session_background.sessions_structure, session_background.base, log = log,
           command_timings = command_timings0)
       val session =
         new Session(options, resources) {
@@ -451,7 +451,7 @@
       val eval_main = Command_Line.ML_tool("Isabelle_Process.init_build ()" :: eval_store)
 
       val process =
-        Isabelle_Process.start(session, options, base_info, store,
+        Isabelle_Process.start(session, options, session_background, store,
           logic = parent, raw_ml_system = is_pure,
           use_prelude = use_prelude, eval_main = eval_main,
           cwd = info.dir.file, env = env)
@@ -489,7 +489,7 @@
           if (build_errors.isInstanceOf[Exn.Res[_]] && process_result.ok && info.documents.nonEmpty) {
             using(Export.open_database_context(store)) { database_context =>
               val documents =
-                using(database_context.open_session(deps.base_info(session_name))) {
+                using(database_context.open_session(deps.background(session_name))) {
                   session_context =>
                     Document_Build.build_documents(
                       Document_Build.context(session_context, progress = progress),

--- 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)
 

--- a/src/Tools/VSCode/src/build_vscode_extension.scala	Fri Dec 16 17:30:29 2022 +0100
+++ b/src/Tools/VSCode/src/build_vscode_extension.scala	Fri Dec 16 17:51:52 2022 +0100
@@ -21,7 +21,7 @@
     progress: Progress = new Progress
   ): Unit = {
     val keywords =
-      Sessions.base_info(options, logic, dirs = dirs).check_errors.base.overall_syntax.keywords
+      Sessions.background(options, logic, dirs = dirs).check_errors.base.overall_syntax.keywords
 
     val output_path = build_dir + Path.explode("isabelle-grammar.json")
     progress.echo(output_path.expand.implode)

--- a/src/Tools/VSCode/src/language_server.scala	Fri Dec 16 17:30:29 2022 +0100
+++ b/src/Tools/VSCode/src/language_server.scala	Fri Dec 16 17:51:52 2022 +0100
@@ -259,19 +259,20 @@
 
     val try_session =
       try {
-        val base_info =
-          Sessions.base_info(
+        val session_background =
+          Sessions.background(
             options, session_name, dirs = session_dirs,
             include_sessions = include_sessions, session_ancestor = session_ancestor,
             session_requirements = session_requirements).check_errors
 
         def build(no_build: Boolean = false): Build.Results =
           Build.build(options,
-            selection = Sessions.Selection.session(base_info.session_name),
-            build_heap = true, no_build = no_build, dirs = session_dirs, infos = base_info.infos)
+            selection = Sessions.Selection.session(session_background.session_name),
+            build_heap = true, no_build = no_build, dirs = session_dirs,
+            infos = session_background.infos)
 
         if (!session_no_build && !build(no_build = true).ok) {
-          val start_msg = "Build started for Isabelle/" + base_info.session_name + " ..."
+          val start_msg = "Build started for Isabelle/" + session_background.session_name + " ..."
           val fail_msg = "Session build failed -- prover process remains inactive!"
 
           val progress = channel.progress(verbose = true)
@@ -281,7 +282,7 @@
         }
 
         val resources =
-          new VSCode_Resources(options, base_info, log) {
+          new VSCode_Resources(options, session_background, log) {
             override def commit(change: Session.Change): Unit =
               if (change.deps_changed || undefined_blobs(change.version).nonEmpty) {
                 delay_load.invoke()
@@ -291,11 +292,11 @@
         val session_options = options.bool("editor_output_state") = true
         val session = new Session(session_options, resources)
 
-        Some((base_info, session))
+        Some((session_background, session))
       }
       catch { case ERROR(msg) => reply_error(msg); None }
 
-    for ((base_info, session) <- try_session) {
+    for ((session_background, session) <- try_session) {
       val store = Sessions.store(options)
 
       session_.change(_ => Some(session))
@@ -306,9 +307,11 @@
       dynamic_output.init()
 
       try {
-        Isabelle_Process.start(session, options, base_info, store,
-          modes = modes, logic = base_info.session_name).await_startup()
-        reply_ok("Welcome to Isabelle/" + base_info.session_name + Isabelle_System.isabelle_heading())
+        Isabelle_Process.start(session, options, session_background, store,
+          modes = modes, logic = session_background.session_name).await_startup()
+        reply_ok(
+          "Welcome to Isabelle/" + session_background.session_name +
+          Isabelle_System.isabelle_heading())
       }
       catch { case ERROR(msg) => reply_error(msg) }
     }

--- a/src/Tools/VSCode/src/vscode_resources.scala	Fri Dec 16 17:30:29 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Fri Dec 16 17:51:52 2022 +0100
@@ -69,11 +69,11 @@
 
 class VSCode_Resources(
   val options: Options,
-  session_base_info: Sessions.Base_Info,
+  session_background: Sessions.Background,
   log: Logger = No_Logger)
 extends Resources(
-  session_base_info.sessions_structure,
-  session_base_info.check_errors.base,
+  session_background.sessions_structure,
+  session_background.check_errors.base,
   log = log
 ) {
   resources =>

--- a/src/Tools/jEdit/src/jedit_resources.scala	Fri Dec 16 17:30:29 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Fri Dec 16 17:51:52 2022 +0100
@@ -23,12 +23,12 @@
 
 object JEdit_Resources {
   def apply(options: Options): JEdit_Resources =
-    new JEdit_Resources(JEdit_Sessions.session_base_info(options))
+    new JEdit_Resources(JEdit_Sessions.session_background(options))
 }
 
-class JEdit_Resources private(val session_base_info: Sessions.Base_Info)
-extends Resources(session_base_info.sessions_structure, session_base_info.base) {
-  def session_errors: List[String] = session_base_info.errors
+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
 
 
   /* document node name */

--- a/src/Tools/jEdit/src/jedit_sessions.scala	Fri Dec 16 17:30:29 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Fri Dec 16 17:51:52 2022 +0100
@@ -122,8 +122,8 @@
 
   /* session build process */
 
-  def session_base_info(options: Options): Sessions.Base_Info =
-    Sessions.base_info(options,
+  def session_background(options: Options): Sessions.Background =
+    Sessions.background(options,
       dirs = JEdit_Sessions.session_dirs,
       include_sessions = logic_include_sessions,
       session = logic_name(options),
@@ -138,18 +138,18 @@
     Build.build(session_options(options),
       selection = Sessions.Selection.session(PIDE.resources.session_base.session_name),
       progress = progress, build_heap = true, no_build = no_build, dirs = session_dirs,
-      infos = PIDE.resources.session_base_info.infos).rc
+      infos = PIDE.resources.session_background.infos).rc
   }
 
   def session_start(options0: Options): Unit = {
     val session = PIDE.session
     val options = session_options(options0)
-    val base_info = PIDE.resources.session_base_info
+    val session_background = PIDE.resources.session_background
     val store = Sessions.store(options)
 
     session.phase_changed += PIDE.plugin.session_phase_changed
 
-    Isabelle_Process.start(session, options, base_info, store,
+    Isabelle_Process.start(session, options, session_background, store,
       logic = PIDE.resources.session_base.session_name,
       modes =
         (space_explode(',', options.string("jedit_print_mode")) :::