# HG changeset patch
# User wenzelm
# Date 1396272877 -7200
# Node ID 520148f9921d037a1d75fbb568b91cd6aa06809d
# Parent  60434514ec0ae0444d00d08cbc569f5e5463de6f
tuned output;

diff -r 60434514ec0a -r 520148f9921d src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Mon Mar 31 15:28:14 2014 +0200
+++ b/src/Pure/PIDE/document.scala	Mon Mar 31 15:34:37 2014 +0200
@@ -303,6 +303,8 @@
 
     def descendants(names: List[Node.Name]): List[Node.Name] = graph.all_succs(names)
     def topological_order: List[Node.Name] = graph.topological_order
+
+    override def toString: String = topological_order.mkString("Nodes(", ",", ")")
   }