tuned output;
authorwenzelm
Thu, 31 Jul 2025 15:19:20 +0200
changeset 82941 f170ec047460
parent 82940 ded486c16c77
child 82942 fb5f91782133
tuned output;
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 */