src/Pure/PIDE/document.scala
changeset 56337 520148f9921d
parent 56336 60434514ec0a
child 56354 a6f8c3566560
     1.1 --- a/src/Pure/PIDE/document.scala	Mon Mar 31 15:28:14 2014 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Mon Mar 31 15:34:37 2014 +0200
     1.3 @@ -303,6 +303,8 @@
     1.4  
     1.5      def descendants(names: List[Node.Name]): List[Node.Name] = graph.all_succs(names)
     1.6      def topological_order: List[Node.Name] = graph.topological_order
     1.7 +
     1.8 +    override def toString: String = topological_order.mkString("Nodes(", ",", ")")
     1.9    }
    1.10  
    1.11