# HG changeset patch
# User wenzelm
# Date 1310731632 -7200
# Node ID 60cd0ac63fdb890bd7143e37a15e64388b13b41b
# Parent  04008ec62370ea4d7927d913e2c2eb5c664d9748
simplified malformed YXML markup -- special controls are visible in IsabelleText font;

diff -r 04008ec62370 -r 60cd0ac63fdb src/Pure/General/yxml.scala
--- 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) }
   }
 }