# HG changeset patch
# User wenzelm
# Date 1396037867 -3600
# Node ID 42df98d4ab5f628cd67afc2ed7f2e64fe3547564
# Parent  4d8955cdfb9798268bb99ad9cd4dac8b336b8e74
tuned;

diff -r 4d8955cdfb97 -r 42df98d4ab5f src/Pure/PIDE/markup_tree.scala
--- a/src/Pure/PIDE/markup_tree.scala	Thu Mar 27 21:38:45 2014 +0100
+++ b/src/Pure/PIDE/markup_tree.scala	Fri Mar 28 21:17:47 2014 +0100
@@ -117,15 +117,18 @@
     this(branches + (entry.range -> entry))
 
   private def overlapping(range: Text.Range): Branches.T =
-  {
-    val start = Text.Range(range.start)
-    val stop = Text.Range(range.stop)
-    val bs = branches.range(start, stop)
-    branches.get(stop) match {
-      case Some(end) if range overlaps end.range => bs + (end.range -> end)
-      case _ => bs
+    if (branches.isEmpty ||
+        (range.contains(branches.firstKey.start) && range.contains(branches.lastKey.stop)))
+      branches
+    else {
+      val start = Text.Range(range.start)
+      val stop = Text.Range(range.stop)
+      val bs = branches.range(start, stop)
+      branches.get(stop) match {
+        case Some(end) if range overlaps end.range => bs + (end.range -> end)
+        case _ => bs
+      }
     }
-  }
 
   def restrict(range: Text.Range): Markup_Tree =
     new Markup_Tree(overlapping(range))