ignore markup elements over empty body, which are not well-defined within markup tree and fail to work with merge_disjoint (e.g. multiple inlined positions);
1.1 --- a/src/Pure/PIDE/markup_tree.scala Sun Dec 30 18:23:31 2012 +0100
1.2 +++ b/src/Pure/PIDE/markup_tree.scala Sun Dec 30 20:15:02 2012 +0100
1.3 @@ -118,9 +118,12 @@
1.4
1.5 case (elems, body) =>
1.6 val (end_offset, subtrees) = ((offset, Nil: List[Markup_Tree]) /: body)(make_trees)
1.7 - val range = Text.Range(offset, end_offset)
1.8 - val entry = Entry(range, elems, merge_disjoint(subtrees))
1.9 - (end_offset, new Markup_Tree(Branches.empty, entry) :: markup_trees)
1.10 + if (offset == end_offset) acc
1.11 + else {
1.12 + val range = Text.Range(offset, end_offset)
1.13 + val entry = Entry(range, elems, merge_disjoint(subtrees))
1.14 + (end_offset, new Markup_Tree(Branches.empty, entry) :: markup_trees)
1.15 + }
1.16 }
1.17 }
1.18