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