src/Tools/jEdit/src/document_model.scala
changeset 64680 7f87c1aa0ffa
parent 64673 b5965890e54d
child 64799 c0c648911f1a
--- a/src/Tools/jEdit/src/document_model.scala	Wed Dec 28 16:45:00 2016 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Wed Dec 28 16:50:14 2016 +0100
@@ -69,6 +69,9 @@
 
 class Document_Model(val session: Session, val buffer: Buffer, val node_name: Document.Node.Name)
 {
+  override def toString: String = node_name.toString
+
+
   /* header */
 
   def is_theory: Boolean = node_name.is_theory