--- 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")
--- 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)
--- 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()
--- 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 || {