changeset 27971 | 57dc3bd6f841 |
parent 27960 | 65b10d8ef0c6 |
child 27993 | 6dd90ef9f927 |
--- a/src/Pure/General/yxml.scala Sat Aug 23 23:07:39 2008 +0200 +++ b/src/Pure/General/yxml.scala Sat Aug 23 23:07:41 2008 +0200 @@ -115,7 +115,7 @@ def parse_failsafe(source: CharSequence) = { try { parse(source) } catch { - case e: BadYXML => XML.Elem (Markup.MALFORMED, Nil, + case e: BadYXML => XML.Elem (Markup.BAD, Nil, List(XML.Text(source.toString.replace(X_string, "\\<^X>").replace(Y_string, "\\<^Y>")))) } }