--- a/src/Pure/PIDE/resources.scala Fri Dec 16 17:51:52 2022 +0100
+++ b/src/Pure/PIDE/resources.scala Fri Dec 16 18:12:48 2022 +0100
@@ -13,7 +13,7 @@
object Resources {
- def bootstrap: Resources = new Resources(Sessions.Structure.empty, Sessions.Base.bootstrap)
+ def bootstrap: Resources = new Resources(Sessions.Background(base = 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)
@@ -23,13 +23,15 @@
}
class Resources(
- val sessions_structure: Sessions.Structure,
- val session_base: Sessions.Base,
+ val session_background: Sessions.Background,
val log: Logger = No_Logger,
command_timings: List[Properties.T] = Nil
) {
resources =>
+ def sessions_structure: Sessions.Structure = session_background.sessions_structure
+ def session_base: Sessions.Base = session_background.base
+ def session_errors: List[String] = session_background.errors
override def toString: String = "Resources(" + session_base.toString + ")"