# HG changeset patch # User wenzelm # Date 1482940214 -3600 # Node ID 7f87c1aa0ffa185bc905465f03bf6a5261b367f5 # Parent b2bf280b7e1312cda7fbf022406a06f2287246fd tuned; diff -r b2bf280b7e13 -r 7f87c1aa0ffa src/Tools/VSCode/src/document_model.scala --- a/src/Tools/VSCode/src/document_model.scala Wed Dec 28 16:45:00 2016 +0100 +++ b/src/Tools/VSCode/src/document_model.scala Wed Dec 28 16:50:14 2016 +0100 @@ -17,6 +17,9 @@ changed: Boolean = true, published_diagnostics: List[Text.Info[Command.Results]] = Nil) { + override def toString: String = node_name.toString + + /* header */ def is_theory: Boolean = node_name.is_theory diff -r b2bf280b7e13 -r 7f87c1aa0ffa src/Tools/jEdit/src/document_model.scala --- 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