diff -r d6a4d7b013f7 -r 65b10d8ef0c6 src/Pure/General/yxml.scala
--- a/src/Pure/General/yxml.scala	Sat Aug 23 19:42:13 2008 +0200
+++ b/src/Pure/General/yxml.scala	Sat Aug 23 19:42:14 2008 +0200
@@ -16,6 +16,7 @@
 
   private val X = '\5'
   private val Y = '\6'
+  private val X_string = X.toString
   private val Y_string = Y.toString
 
   def detect(source: CharSequence) = {
@@ -110,4 +111,13 @@
       case Nil => XML.Text("")
       case _ => err("multiple results")
     }
+
+  def parse_failsafe(source: CharSequence) = {
+    try { parse(source) }
+    catch {
+      case e: BadYXML => XML.Elem (Markup.MALFORMED, Nil,
+        List(XML.Text(source.toString.replace(X_string, "\\<^X>").replace(Y_string, "\\<^Y>"))))
+    }
+  }
+
 }