changeset 64680 | 7f87c1aa0ffa |
parent 64679 | b2bf280b7e13 |
child 64682 | 7e119f32276a |
--- 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