tuned;
authorwenzelm
Fri Mar 28 21:17:47 2014 +0100 (2014-03-28)
changeset 5631142df98d4ab5f
parent 56310 4d8955cdfb97
child 56312 b61fd2507006
child 56313 84d047625f70
tuned;
src/Pure/PIDE/markup_tree.scala
     1.1 --- a/src/Pure/PIDE/markup_tree.scala	Thu Mar 27 21:38:45 2014 +0100
     1.2 +++ b/src/Pure/PIDE/markup_tree.scala	Fri Mar 28 21:17:47 2014 +0100
     1.3 @@ -117,15 +117,18 @@
     1.4      this(branches + (entry.range -> entry))
     1.5  
     1.6    private def overlapping(range: Text.Range): Branches.T =
     1.7 -  {
     1.8 -    val start = Text.Range(range.start)
     1.9 -    val stop = Text.Range(range.stop)
    1.10 -    val bs = branches.range(start, stop)
    1.11 -    branches.get(stop) match {
    1.12 -      case Some(end) if range overlaps end.range => bs + (end.range -> end)
    1.13 -      case _ => bs
    1.14 +    if (branches.isEmpty ||
    1.15 +        (range.contains(branches.firstKey.start) && range.contains(branches.lastKey.stop)))
    1.16 +      branches
    1.17 +    else {
    1.18 +      val start = Text.Range(range.start)
    1.19 +      val stop = Text.Range(range.stop)
    1.20 +      val bs = branches.range(start, stop)
    1.21 +      branches.get(stop) match {
    1.22 +        case Some(end) if range overlaps end.range => bs + (end.range -> end)
    1.23 +        case _ => bs
    1.24 +      }
    1.25      }
    1.26 -  }
    1.27  
    1.28    def restrict(range: Text.Range): Markup_Tree =
    1.29      new Markup_Tree(overlapping(range))