simplified malformed YXML markup -- special controls are visible in IsabelleText font;
--- a/src/Pure/General/yxml.scala Fri Jul 15 13:29:00 2011 +0200
+++ b/src/Pure/General/yxml.scala Fri Jul 15 14:07:12 2011 +0200
@@ -117,19 +117,18 @@
/* failsafe parsing */
- private def markup_failsafe(source: CharSequence) =
- XML.elem (Markup.MALFORMED,
- List(XML.Text(source.toString.replace(X_string, "\\<^X>").replace(Y_string, "\\<^Y>"))))
+ private def markup_malformed(source: CharSequence) =
+ XML.elem(Markup.MALFORMED, List(XML.Text(source.toString)))
def parse_body_failsafe(source: CharSequence): XML.Body =
{
try { parse_body(source) }
- catch { case ERROR(_) => List(markup_failsafe(source)) }
+ catch { case ERROR(_) => List(markup_malformed(source)) }
}
def parse_failsafe(source: CharSequence): XML.Tree =
{
try { parse(source) }
- catch { case ERROR(_) => markup_failsafe(source) }
+ catch { case ERROR(_) => markup_malformed(source) }
}
}