# HG changeset patch # User wenzelm # Date 1219525661 -7200 # Node ID 57dc3bd6f841c703a54a22f3dfecb1988f0f6380 # Parent 3dd5fbdf61c481089514f4043daca220684ba969 renamed Markup.MALFORMED to Markup.BAD; diff -r 3dd5fbdf61c4 -r 57dc3bd6f841 src/Pure/General/yxml.scala --- 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>")))) } }