diff -r ed147003de4b -r 968844caaff9 src/Pure/General/yxml.scala --- a/src/Pure/General/yxml.scala Sat Aug 07 22:09:52 2010 +0200 +++ b/src/Pure/General/yxml.scala Sat Aug 07 22:43:57 2010 +0200 @@ -117,7 +117,7 @@ /* failsafe parsing */ private def markup_failsafe(source: CharSequence) = - XML.Elem (Markup(Markup.MALFORMED, Nil), + XML.elem (Markup.MALFORMED, List(XML.Text(source.toString.replace(X_string, "\\<^X>").replace(Y_string, "\\<^Y>")))) def parse_body_failsafe(source: CharSequence): List[XML.Tree] =