# HG changeset patch
# User wenzelm
# Date 1671206530 -3600
# Node ID a3177042863d869e9ccff3711d9890734a0a7cb6
# Parent  f8b1a75dbea76bf37d7d020b2c05d728892b5dac
tuned signature;

diff -r f8b1a75dbea7 -r a3177042863d src/Pure/ML/ml_process.scala
--- a/src/Pure/ML/ml_process.scala	Fri Dec 16 16:00:56 2022 +0100
+++ b/src/Pure/ML/ml_process.scala	Fri Dec 16 17:02:10 2022 +0100
@@ -80,7 +80,7 @@
     // session base
     val (init_session_base, eval_init_session) =
       session_base match {
-        case None => (Sessions.bootstrap_base, Nil)
+        case None => (Sessions.Base.bootstrap, Nil)
         case Some(base) => (base, List("Resources.init_session_env ()"))
       }
     val init_session = Isabelle_System.tmp_file("init_session")
diff -r f8b1a75dbea7 -r a3177042863d src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Fri Dec 16 16:00:56 2022 +0100
+++ b/src/Pure/PIDE/resources.scala	Fri Dec 16 17:02:10 2022 +0100
@@ -13,7 +13,7 @@
 
 
 object Resources {
-  def empty: Resources = new Resources(Sessions.Structure.empty, Sessions.bootstrap_base)
+  def bootstrap: Resources = new Resources(Sessions.Structure.empty, 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)
diff -r f8b1a75dbea7 -r a3177042863d src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Fri Dec 16 16:00:56 2022 +0100
+++ b/src/Pure/Thy/sessions.scala	Fri Dec 16 17:02:10 2022 +0100
@@ -56,6 +56,10 @@
 
   /* base info */
 
+  object Base {
+    val bootstrap: Base = Base(overall_syntax = Thy_Header.bootstrap_syntax)
+  }
+
   sealed case class Base(
     session_name: String = "",
     session_pos: Position.T = Position.none,
@@ -97,8 +101,6 @@
       nodes(name).syntax orElse loaded_theory_syntax(name) getOrElse overall_syntax
   }
 
-  val bootstrap_base: Base = Base(overall_syntax = Thy_Header.bootstrap_syntax)
-
   sealed case class Base_Info(
     base: Base,
     sessions_structure: Structure = Structure.empty,
@@ -257,7 +259,7 @@
 
     val session_bases =
       sessions_structure.imports_topological_order.foldLeft(
-          Map(Sessions.bootstrap_base.session_entry)) {
+          Map(Sessions.Base.bootstrap.session_entry)) {
         case (session_bases, session_name) =>
           progress.expose_interrupt()
 
diff -r f8b1a75dbea7 -r a3177042863d src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Fri Dec 16 16:00:56 2022 +0100
+++ b/src/Pure/Tools/build_job.scala	Fri Dec 16 17:02:10 2022 +0100
@@ -99,7 +99,7 @@
     unicode_symbols: Boolean = false
   ): Unit = {
     val store = Sessions.store(options)
-    val session = new Session(options, Resources.empty)
+    val session = new Session(options, Resources.bootstrap)
 
     def check(filter: List[Regex], make_string: => String): Boolean =
       filter.isEmpty || {