src/Pure/PIDE/markup_tree.scala
changeset 52642 84eb792224a8
parent 51618 a3577cd80c41
child 52889 ea3338812e67
     1.1 --- a/src/Pure/PIDE/markup_tree.scala	Sat Jul 13 00:50:49 2013 +0200
     1.2 +++ b/src/Pure/PIDE/markup_tree.scala	Sat Jul 13 12:39:45 2013 +0200
     1.3 @@ -184,6 +184,10 @@
     1.4      }
     1.5    }
     1.6  
     1.7 +  def ++ (other: Markup_Tree): Markup_Tree =
     1.8 +    (this /: other.branches)({ case (tree, (range, entry)) =>
     1.9 +      ((tree ++ entry.subtree) /: entry.markup)({ case (t, elem) => t + Text.Info(range, elem) }) })
    1.10 +
    1.11    def to_XML(root_range: Text.Range, text: CharSequence, filter: XML.Elem => Boolean): XML.Body =
    1.12    {
    1.13      def make_text(start: Text.Offset, stop: Text.Offset): XML.Body =