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