# HG changeset patch # User wenzelm # Date 1314908997 -7200 # Node ID 446fe2abe25227e31874530b926f798a300bc918 # Parent 101c117494cd9fe15bd6bf33f4316fbffb07e9aa more redable Document.Node.toString; diff -r 101c117494cd -r 446fe2abe252 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Thu Sep 01 16:58:41 2011 +0200 +++ b/src/Pure/PIDE/document.scala Thu Sep 01 22:29:57 2011 +0200 @@ -47,6 +47,7 @@ case other: Name => node == other.node case _ => false } + override def toString: String = theory } sealed abstract class Edit[A, B]