--- a/src/Pure/PIDE/yxml.scala Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/PIDE/yxml.scala Mon Nov 28 22:05:32 2011 +0100
@@ -118,18 +118,18 @@
/* failsafe parsing */
- private def markup_malformed(source: CharSequence) =
- XML.elem(Markup.MALFORMED, List(XML.Text(source.toString)))
+ private def markup_broken(source: CharSequence) =
+ XML.elem(Markup.Broken.name, List(XML.Text(source.toString)))
def parse_body_failsafe(source: CharSequence): XML.Body =
{
try { parse_body(source) }
- catch { case ERROR(_) => List(markup_malformed(source)) }
+ catch { case ERROR(_) => List(markup_broken(source)) }
}
def parse_failsafe(source: CharSequence): XML.Tree =
{
try { parse(source) }
- catch { case ERROR(_) => markup_malformed(source) }
+ catch { case ERROR(_) => markup_broken(source) }
}
}