src/Pure/PIDE/markup_tree.scala
changeset 38562 3de5f0424caa
parent 38486 f5bbfc019937
child 38563 f6c9a4f9f66f
     1.1 --- a/src/Pure/PIDE/markup_tree.scala	Thu Aug 19 18:44:26 2010 +0200
     1.2 +++ b/src/Pure/PIDE/markup_tree.scala	Thu Aug 19 22:04:20 2010 +0200
     1.3 @@ -20,7 +20,7 @@
     1.4    case class Node(val range: Text.Range, val info: Any)
     1.5    {
     1.6      def contains(that: Node): Boolean = this.range contains that.range
     1.7 -    def intersect(r: Text.Range): Node = Node(range.intersect(r), info)
     1.8 +    def restrict(r: Text.Range): Node = Node(range.intersect(r), info)
     1.9    }
    1.10  
    1.11  
    1.12 @@ -35,8 +35,11 @@
    1.13        {
    1.14          def compare(x: Node, y: Node): Int = x.range compare y.range
    1.15        })
    1.16 -    def update(branches: T, entries: Entry*): T =
    1.17 -      branches ++ entries.map(e => (e._1 -> e))
    1.18 +
    1.19 +    def update(branches: T, entry: Entry): T = branches + (entry._1 -> entry)
    1.20 +
    1.21 +    def overlapping(range: Text.Range, branches: T): T =
    1.22 +      branches.range(Node(range.start_range, Nil), Node(range.stop_range, Nil))
    1.23    }
    1.24  
    1.25    val empty = new Markup_Tree(Branches.empty)
    1.26 @@ -58,14 +61,11 @@
    1.27          else if (new_node.contains(branches.head._1) && new_node.contains(branches.last._1))
    1.28            new Markup_Tree(Branches.update(Branches.empty, (new_node -> this)))
    1.29          else {
    1.30 -          var overlapping = Branches.empty
    1.31 -          var rest = branches
    1.32 -          while (rest.isDefinedAt(new_node)) {
    1.33 -            overlapping = Branches.update(overlapping, rest(new_node))
    1.34 -            rest -= new_node
    1.35 +          val body = Branches.overlapping(new_node.range, branches)
    1.36 +          if (body.forall(e => new_node.contains(e._1))) {
    1.37 +            val rest = (branches /: body) { case (bs, (e, _)) => bs - e }
    1.38 +            new Markup_Tree(Branches.update(rest, new_node -> new Markup_Tree(body)))
    1.39            }
    1.40 -          if (overlapping.forall(e => new_node.contains(e._1)))
    1.41 -            new Markup_Tree(Branches.update(rest, new_node -> new Markup_Tree(overlapping)))
    1.42            else { // FIXME split markup!?
    1.43              System.err.println("Ignored overlapping markup: " + new_node)
    1.44              this
    1.45 @@ -105,30 +105,26 @@
    1.46    {
    1.47      def stream(parent: Node, bs: Branches.T): Stream[Node] =
    1.48      {
    1.49 -      val start = Node(parent.range.start_range, Nil)
    1.50 -      val stop = Node(parent.range.stop_range, Nil)
    1.51        val substream =
    1.52 -        (for ((_, (node, subtree)) <- bs.range(start, stop).toStream) yield {
    1.53 +        (for ((_, (node, subtree)) <- Branches.overlapping(parent.range, bs).toStream) yield {
    1.54            if (sel.isDefinedAt(node))
    1.55 -            stream(node.intersect(parent.range), subtree.branches)
    1.56 +            stream(node.restrict(parent.range), subtree.branches)
    1.57            else stream(parent, subtree.branches)
    1.58          }).flatten
    1.59  
    1.60        def padding(last: Text.Offset, s: Stream[Node]): Stream[Node] =
    1.61          s match {
    1.62 -          case node #:: rest =>
    1.63 -            if (last < node.range.start)
    1.64 -              parent.intersect(Text.Range(last, node.range.start)) #::
    1.65 -                node #:: padding(node.range.stop, rest)
    1.66 -            else node #:: padding(node.range.stop, rest)
    1.67 +          case (node @ Node(Text.Range(start, stop), _)) #:: rest =>
    1.68 +            if (last < start)
    1.69 +              parent.restrict(Text.Range(last, start)) #:: node #:: padding(stop, rest)
    1.70 +            else node #:: padding(stop, rest)
    1.71            case Stream.Empty =>  // FIXME
    1.72              if (last < parent.range.stop)
    1.73 -            Stream(parent.intersect(Text.Range(last, parent.range.stop)))
    1.74 +              Stream(parent.restrict(Text.Range(last, parent.range.stop)))
    1.75              else Stream.Empty
    1.76          }
    1.77        padding(parent.range.start, substream)
    1.78      }
    1.79 -    // FIXME handle disjoint range!?
    1.80      stream(Node(range, Nil), branches)
    1.81    }
    1.82