src/Pure/PIDE/markup_tree.scala
changeset 45473 66395afbd915
parent 45470 81b85d4ed269
child 45474 f793dd5d84b2
     1.1 --- a/src/Pure/PIDE/markup_tree.scala	Sat Nov 12 18:05:31 2011 +0100
     1.2 +++ b/src/Pure/PIDE/markup_tree.scala	Sat Nov 12 18:56:49 2011 +0100
     1.3 @@ -20,6 +20,12 @@
     1.4  
     1.5    val empty: Markup_Tree = new Markup_Tree(Branches.empty)
     1.6  
     1.7 +  object Entry
     1.8 +  {
     1.9 +    def apply(markup: Text.Markup, subtree: Markup_Tree): Entry =
    1.10 +      Entry(markup.range, List(markup.info), subtree)
    1.11 +  }
    1.12 +
    1.13    sealed case class Entry(range: Text.Range, rev_markup: List[XML.Elem], subtree: Markup_Tree)
    1.14    {
    1.15      def + (m: XML.Elem): Entry = copy(rev_markup = m :: rev_markup)
    1.16 @@ -63,18 +69,16 @@
    1.17    def + (new_markup: Text.Markup): Markup_Tree =
    1.18    {
    1.19      val new_range = new_markup.range
    1.20 -    val new_info = new_markup.info
    1.21  
    1.22      branches.get(new_range) match {
    1.23 -      case None =>
    1.24 -        new Markup_Tree(branches, Entry(new_range, List(new_info), empty))
    1.25 +      case None => new Markup_Tree(branches, Entry(new_markup, empty))
    1.26        case Some(entry) =>
    1.27          if (entry.range == new_range)
    1.28 -          new Markup_Tree(branches, entry + new_info)
    1.29 +          new Markup_Tree(branches, entry + new_markup.info)
    1.30          else if (entry.range.contains(new_range))
    1.31            new Markup_Tree(branches, entry.copy(subtree = entry.subtree + new_markup))
    1.32          else if (new_range.contains(branches.head._1) && new_range.contains(branches.last._1))
    1.33 -          new Markup_Tree(Branches.empty, Entry(new_range, List(new_info), this))
    1.34 +          new Markup_Tree(Branches.empty, Entry(new_markup, this))
    1.35          else {
    1.36            val body = overlapping(new_range)
    1.37            if (body.forall(e => new_range.contains(e._1))) {
    1.38 @@ -83,7 +87,7 @@
    1.39                  (Branches.empty /: branches)((rest, entry) =>
    1.40                    if (body.isDefinedAt(entry._1)) rest else rest + entry)
    1.41                else branches
    1.42 -            new Markup_Tree(rest, Entry(new_range, List(new_info), new Markup_Tree(body)))
    1.43 +            new Markup_Tree(rest, Entry(new_markup, new Markup_Tree(body)))
    1.44            }
    1.45            else { // FIXME split markup!?
    1.46              System.err.println("Ignored overlapping markup information: " + new_markup)