src/Pure/General/yxml.scala
changeset 43841 60cd0ac63fdb
parent 43782 834de29572d5
child 44181 bbce0417236d
--- 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) }
   }
 }