# HG changeset patch
# User wenzelm
# Date 1753967960 -7200
# Node ID f170ec047460434aedfec73cf04d44d590c6d34a
# Parent  ded486c16c77b2b246658a1f9f54c12353592fd6
tuned output;

diff -r ded486c16c77 -r f170ec047460 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Thu Jul 31 13:41:43 2025 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Thu Jul 31 15:19:20 2025 +0200
@@ -408,7 +408,7 @@
   last_perspective: Document.Node.Perspective_Text.T,
   pending_edits: List[Text.Edit]
 ) extends Document_Model {
-  override def toString: String = "file " + quote(super.toString)
+  override def toString: String = "file " + quote(node_name.node)
 
 
   /* content */
@@ -493,7 +493,7 @@
   val node_name: Document.Node.Name,
   val buffer: Buffer
 ) extends Document_Model {
-  override def toString: String = "buffer " + quote(super.toString)
+  override def toString: String = "buffer " + quote(node_name.node)
 
 
   /* text */