src/Pure/PIDE/resources.scala
changeset 75768 be79948f7f23
parent 75752 a0253e471aa4
child 75884 3d8b37b1d798
--- 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 = {