# HG changeset patch
# User wenzelm
# Date 1659717949 -7200
# Node ID be79948f7f23c8b851554956cefc8ab4ba802665
# Parent  87f9748b214ac9cc1f0ffd7c8748b9d853226bb8
clarified signature: more operations;

diff -r 87f9748b214a -r be79948f7f23 src/Pure/PIDE/resources.scala
--- 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 = {
diff -r 87f9748b214a -r be79948f7f23 src/Pure/Thy/sessions.scala
--- 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,