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);
authorwenzelm
Sun Dec 30 20:15:02 2012 +0100 (2012-12-30)
changeset 50642aca12f646772
parent 50641 b908e56e83ca
child 50643 09394eaf6804
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);
src/Pure/PIDE/markup_tree.scala
     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