src/Pure/PIDE/markup_tree.scala
changeset 38563 f6c9a4f9f66f
parent 38562 3de5f0424caa
child 38564 a6e2715fac5f
     1.1 --- a/src/Pure/PIDE/markup_tree.scala	Thu Aug 19 22:04:20 2010 +0200
     1.2 +++ b/src/Pure/PIDE/markup_tree.scala	Thu Aug 19 22:26:15 2010 +0200
     1.3 @@ -50,6 +50,12 @@
     1.4  {
     1.5    import Markup_Tree._
     1.6  
     1.7 +  override def toString =
     1.8 +    branches.toList.map(_._2) match {
     1.9 +      case Nil => "Empty"
    1.10 +      case list => list.mkString("Tree(", ",", ")")
    1.11 +    }
    1.12 +
    1.13    def + (new_node: Node): Markup_Tree =
    1.14    {
    1.15      branches.get(new_node) match {