1.1 --- a/src/Pure/PIDE/markup_tree.scala	Fri Sep 28 17:06:07 2012 +0200
     1.2 +++ b/src/Pure/PIDE/markup_tree.scala	Fri Sep 28 22:53:18 2012 +0200
     1.3 @@ -66,11 +66,14 @@
     1.4  
     1.5    /* XML representation */
     1.6  
     1.7 -  // FIXME decode markup body
     1.8 -  @tailrec private def strip_elems(markups: List[Markup], body: XML.Body): (List[Markup], XML.Body) =
     1.9 +  @tailrec private def strip_elems(
    1.10 +      elems: List[XML.Elem], body: XML.Body): (List[XML.Elem], XML.Body) =
    1.11      body match {
    1.12 -      case List(XML.Elem(markup1, body1)) => strip_elems(markup1 :: markups, body1)
    1.13 -      case _ => (markups, body)
    1.14 +      case List(XML.Wrapped_Elem(markup1, body1, body2)) =>
    1.15 +        strip_elems(XML.Elem(markup1, body1) :: elems, body2)
    1.16 +      case List(XML.Elem(markup1, body1)) =>
    1.17 +        strip_elems(XML.Elem(markup1, Nil) :: elems, body1)
    1.18 +      case _ => (elems, body)
    1.19      }
    1.20  
    1.21    private def make_trees(acc: (Int, List[Markup_Tree]), tree: XML.Tree): (Int, List[Markup_Tree]) =
    1.22 @@ -84,7 +87,7 @@
    1.23          case (elems, body) =>
    1.24            val (end_offset, subtrees) = ((offset, Nil: List[Markup_Tree]) /: body)(make_trees)
    1.25            val range = Text.Range(offset, end_offset)
    1.26 -          val entry = Entry(range, elems.map(XML.Elem(_, Nil)), merge_disjoint(subtrees))
    1.27 +          val entry = Entry(range, elems, merge_disjoint(subtrees))
    1.28            (end_offset, new Markup_Tree(Branches.empty, entry) :: markup_trees)
    1.29        }
    1.30      }
    1.31 @@ -152,8 +155,10 @@
    1.32  
    1.33      def make_elems(rev_markups: List[XML.Elem], body: XML.Body): XML.Body =
    1.34        (body /: rev_markups) {
    1.35 -        case (b, elem) => // FIXME encode markup body
    1.36 -          if (filter(elem)) List(XML.Elem(elem.markup, b)) else b
    1.37 +        case (b, elem) =>
    1.38 +          if (!filter(elem)) b
    1.39 +          else if (elem.body.isEmpty) List(XML.Elem(elem.markup, b))
    1.40 +          else List(XML.Wrapped_Elem(elem.markup, elem.body, b))
    1.41        }
    1.42  
    1.43      def make_body(elem_range: Text.Range, elem_markup: List[XML.Elem], entries: Branches.T)