renamed Markup.MALFORMED to Markup.BAD;
authorwenzelm
Sat Aug 23 23:07:41 2008 +0200 (2008-08-23)
changeset 2797157dc3bd6f841
parent 27970 3dd5fbdf61c4
child 27972 a87be8fcb25c
renamed Markup.MALFORMED to Markup.BAD;
src/Pure/General/yxml.scala
     1.1 --- a/src/Pure/General/yxml.scala	Sat Aug 23 23:07:39 2008 +0200
     1.2 +++ b/src/Pure/General/yxml.scala	Sat Aug 23 23:07:41 2008 +0200
     1.3 @@ -115,7 +115,7 @@
     1.4    def parse_failsafe(source: CharSequence) = {
     1.5      try { parse(source) }
     1.6      catch {
     1.7 -      case e: BadYXML => XML.Elem (Markup.MALFORMED, Nil,
     1.8 +      case e: BadYXML => XML.Elem (Markup.BAD, Nil,
     1.9          List(XML.Text(source.toString.replace(X_string, "\\<^X>").replace(Y_string, "\\<^Y>"))))
    1.10      }
    1.11    }