src/Pure/PIDE/markup_tree.scala
changeset 38563 f6c9a4f9f66f
parent 38562 3de5f0424caa
child 38564 a6e2715fac5f
equal deleted inserted replaced
38562:3de5f0424caa 38563:f6c9a4f9f66f
    47 
    47 
    48 
    48 
    49 case class Markup_Tree(val branches: Markup_Tree.Branches.T)
    49 case class Markup_Tree(val branches: Markup_Tree.Branches.T)
    50 {
    50 {
    51   import Markup_Tree._
    51   import Markup_Tree._
       
    52 
       
    53   override def toString =
       
    54     branches.toList.map(_._2) match {
       
    55       case Nil => "Empty"
       
    56       case list => list.mkString("Tree(", ",", ")")
       
    57     }
    52 
    58 
    53   def + (new_node: Node): Markup_Tree =
    59   def + (new_node: Node): Markup_Tree =
    54   {
    60   {
    55     branches.get(new_node) match {
    61     branches.get(new_node) match {
    56       case None =>
    62       case None =>