--- a/src/Pure/PIDE/resources.scala Fri Aug 05 17:16:37 2022 +0200
+++ b/src/Pure/PIDE/resources.scala Fri Aug 05 18:45:49 2022 +0200
@@ -35,6 +35,9 @@
resources =>
+ override def toString: String = "Resources(" + session_base.toString + ")"
+
+
/* init session */
def init_session_yxml: String = {
--- a/src/Pure/Thy/sessions.scala Fri Aug 05 17:16:37 2022 +0200
+++ b/src/Pure/Thy/sessions.scala Fri Aug 05 18:45:49 2022 +0200
@@ -373,6 +373,7 @@
) {
def check: Base_Info = if (errors.isEmpty) this else error(cat_lines(errors))
def session: String = base.session_name
+ lazy val resources: Resources = new Resources(sessions_structure, check.base)
}
def base_info(options: Options,