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