tuned;

--- 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))