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

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