--- a/src/Pure/PIDE/markup_tree.scala Sun Dec 30 18:23:31 2012 +0100
+++ b/src/Pure/PIDE/markup_tree.scala Sun Dec 30 20:15:02 2012 +0100
@@ -118,9 +118,12 @@
case (elems, body) =>
val (end_offset, subtrees) = ((offset, Nil: List[Markup_Tree]) /: body)(make_trees)
- val range = Text.Range(offset, end_offset)
- val entry = Entry(range, elems, merge_disjoint(subtrees))
- (end_offset, new Markup_Tree(Branches.empty, entry) :: markup_trees)
+ if (offset == end_offset) acc
+ else {
+ val range = Text.Range(offset, end_offset)
+ val entry = Entry(range, elems, merge_disjoint(subtrees))
+ (end_offset, new Markup_Tree(Branches.empty, entry) :: markup_trees)
+ }
}
}