--- a/src/Pure/PIDE/resources.scala Sat Dec 17 10:18:12 2022 +0100
+++ b/src/Pure/PIDE/resources.scala Sat Dec 17 11:25:10 2022 +0100
@@ -33,7 +33,7 @@
def session_base: Sessions.Base = session_background.base
def session_errors: List[String] = session_background.errors
- override def toString: String = "Resources(" + session_base.toString + ")"
+ override def toString: String = "Resources(" + session_base.print_body + ")"
/* init session */
--- a/src/Pure/Thy/sessions.scala Sat Dec 17 10:18:12 2022 +0100
+++ b/src/Pure/Thy/sessions.scala Sat Dec 17 11:25:10 2022 +0100
@@ -78,10 +78,11 @@
) {
def session_entry: (String, Base) = session_name -> this
- override def toString: String =
- "Sessions.Base(session_name = " + quote(session_name) +
- ", loaded_theories = " + loaded_theories.size +
- ", used_theories = " + used_theories.length + ")"
+ override def toString: String = "Sessions.Base(" + print_body + ")"
+ def print_body: String =
+ "session_name = " + quote(session_name) +
+ ", loaded_theories = " + loaded_theories.size +
+ ", used_theories = " + used_theories.length
def all_document_theories: List[Document.Node.Name] =
proper_session_theories ::: document_theories