# HG changeset patch # User wenzelm # Date 1356894902 -3600 # Node ID aca12f6467729fcd3f946673f1c7db4be36b1916 # Parent b908e56e83ca1ea7e90fa0137e0dd84c7a6ac0ec 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); diff -r b908e56e83ca -r aca12f646772 src/Pure/PIDE/markup_tree.scala --- 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) + } } }