src/Tools/jEdit/src/prover/MarkupNode.scala
changeset 34706 cce1dcc923dc
parent 34705 cd2cdf3b33b9
child 34707 cc5d388fcbf2
equal deleted inserted replaced
34705:cd2cdf3b33b9 34706:cce1dcc923dc
    67       System.err.println("ignored nonfitting markup: " + new_child)
    67       System.err.println("ignored nonfitting markup: " + new_child)
    68       this
    68       this
    69     }
    69     }
    70   }
    70   }
    71 
    71 
    72   def dfs: List[MarkupNode] = {
       
    73     var all = Nil : List[MarkupNode]
       
    74     for (child <- children)
       
    75       all = child.dfs ::: all
       
    76     all = this :: all
       
    77     all
       
    78   }
       
    79 
       
    80   def leafs: List[MarkupNode] =
       
    81   {
       
    82     if (children.isEmpty) return List(this)
       
    83     else return children flatMap (_.leafs)
       
    84   }
       
    85 
       
    86   def flatten: List[MarkupNode] = {
    72   def flatten: List[MarkupNode] = {
    87     var next_x = start
    73     var next_x = start
    88     if (children.isEmpty) List(this)
    74     if (children.isEmpty) List(this)
    89     else {
    75     else {
    90       val filled_gaps = for {
    76       val filled_gaps = for {