# HG changeset patch
# User wenzelm
# Date 1753962103 -7200
# Node ID ded486c16c77b2b246658a1f9f54c12353592fd6
# Parent  471a1f2844379b83ea00863a4b4a77955bacb1d9
tuned output;

diff -r 471a1f284437 -r ded486c16c77 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Wed Jul 30 15:50:11 2025 +0200
+++ b/src/Pure/PIDE/session.scala	Thu Jul 31 13:41:43 2025 +0200
@@ -136,6 +136,8 @@
 abstract class Session extends Document.Session {
   session =>
 
+  override def toString: String = resources.session_base.session_name
+
   def session_options: Options
   def resources: Resources
 
diff -r 471a1f284437 -r ded486c16c77 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Wed Jul 30 15:50:11 2025 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Thu Jul 31 13:41:43 2025 +0200
@@ -408,6 +408,9 @@
   last_perspective: Document.Node.Perspective_Text.T,
   pending_edits: List[Text.Edit]
 ) extends Document_Model {
+  override def toString: String = "file " + quote(super.toString)
+
+
   /* content */
 
   def node_name: Document.Node.Name = content.node_name
@@ -490,6 +493,9 @@
   val node_name: Document.Node.Name,
   val buffer: Buffer
 ) extends Document_Model {
+  override def toString: String = "buffer " + quote(super.toString)
+
+
   /* text */
 
   def get_text(range: Text.Range): Option[String] =