tuned Markup_Tree, using SortedMap more carefully;
authorwenzelm
Thu Aug 19 12:41:40 2010 +0200 (2010-08-19)
changeset 384827b6ee937b75f
parent 38481 81ec258c4cd3
child 38483 3d16bebee1d3
tuned Markup_Tree, using SortedMap more carefully;
src/Pure/PIDE/markup_tree.scala
     1.1 --- a/src/Pure/PIDE/markup_tree.scala	Thu Aug 19 11:28:51 2010 +0200
     1.2 +++ b/src/Pure/PIDE/markup_tree.scala	Thu Aug 19 12:41:40 2010 +0200
     1.3 @@ -18,6 +18,9 @@
     1.4  object Markup_Tree
     1.5  {
     1.6    case class Node(val range: Text.Range, val info: Any)
     1.7 +  {
     1.8 +    def contains(that: Node): Boolean = this.range contains that.range
     1.9 +  }
    1.10  
    1.11  
    1.12    /* branches sorted by quasi-order -- overlapping intervals appear as equivalent */
    1.13 @@ -33,7 +36,6 @@
    1.14        })
    1.15      def update(branches: T, entries: Entry*): T =
    1.16        branches ++ entries.map(e => (e._1 -> e))
    1.17 -    def make(entries: List[Entry]): T = update(empty, entries:_*)
    1.18    }
    1.19  
    1.20    val empty = new Markup_Tree(Branches.empty)
    1.21 @@ -46,31 +48,28 @@
    1.22  
    1.23    def + (new_node: Node): Markup_Tree =
    1.24    {
    1.25 -    // FIXME tune overlapping == branches && rest.isEmpty
    1.26 -    val (overlapping, rest) =
    1.27 -    {
    1.28 -      val overlapping = new mutable.ListBuffer[Branches.Entry]
    1.29 -      var rest = branches
    1.30 -      while (rest.isDefinedAt(new_node)) {
    1.31 -        overlapping += rest(new_node)
    1.32 -        rest -= new_node
    1.33 -      }
    1.34 -      (overlapping.toList, rest)
    1.35 -    }
    1.36 -    overlapping match {
    1.37 -      case Nil =>
    1.38 +    branches.get(new_node) match {
    1.39 +      case None =>
    1.40          new Markup_Tree(Branches.update(branches, new_node -> empty))
    1.41 -
    1.42 -      case List((node, subtree))
    1.43 -        if node.range != new_node.range && (node.range contains new_node.range) =>
    1.44 -        new Markup_Tree(Branches.update(branches, node -> (subtree + new_node)))
    1.45 -
    1.46 -      case _ if overlapping.forall(e => new_node.range contains e._1.range) =>
    1.47 -        val new_tree = new Markup_Tree(Branches.make(overlapping))
    1.48 -        new Markup_Tree(Branches.update(rest, new_node -> new_tree))
    1.49 -
    1.50 -      case _ => // FIXME split markup!?
    1.51 -        System.err.println("Ignored overlapping markup: " + new_node); this
    1.52 +      case Some((node, subtree)) =>
    1.53 +        if (node.range != new_node.range && node.contains(new_node))
    1.54 +          new Markup_Tree(Branches.update(branches, node -> (subtree + new_node)))
    1.55 +        else if (new_node.contains(branches.head._1) && new_node.contains(branches.last._1))
    1.56 +          new Markup_Tree(Branches.update(Branches.empty, (new_node -> this)))
    1.57 +        else {
    1.58 +          var overlapping = Branches.empty
    1.59 +          var rest = branches
    1.60 +          while (rest.isDefinedAt(new_node)) {
    1.61 +            overlapping = Branches.update(overlapping, rest(new_node))
    1.62 +            rest -= new_node
    1.63 +          }
    1.64 +          if (overlapping.forall(e => new_node.contains(e._1)))
    1.65 +            new Markup_Tree(Branches.update(rest, new_node -> new Markup_Tree(overlapping)))
    1.66 +          else { // FIXME split markup!?
    1.67 +            System.err.println("Ignored overlapping markup: " + new_node)
    1.68 +            this
    1.69 +          }
    1.70 +        }
    1.71      }
    1.72    }
    1.73