tuned output;

--- 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(", ",", ")")
   }