| changeset 57912 | dd9550f84106 | 
| parent 56782 | 433cf57550fa | 
| child 58463 | 0bf0e9788d54 | 
--- a/src/Pure/PIDE/markup_tree.scala Tue Aug 12 15:31:24 2014 +0200 +++ b/src/Pure/PIDE/markup_tree.scala Tue Aug 12 15:46:20 2014 +0200 @@ -261,7 +261,7 @@ make_body(root_range, Nil, overlapping(root_range)) } - override def toString = + override def toString: String = branches.toList.map(_._2) match { case Nil => "Empty" case list => list.mkString("Tree(", ",", ")")