changeset 38231 | 968844caaff9 |
parent 38230 | ed147003de4b |
child 38234 | 4b610fbb2d83 |
--- 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] =