--- 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 */