# HG changeset patch
# User wenzelm
# Date 1232142851 -3600
# Node ID 736bf7117153ae162af69270ceea01257ae0229d
# Parent  7402322256b04b03ec10826bddb1833d5ea47842
added parse_body_failsafe;

diff -r 7402322256b0 -r 736bf7117153 src/Pure/General/yxml.scala
--- a/src/Pure/General/yxml.scala	Fri Jan 16 21:24:33 2009 +0100
+++ b/src/Pure/General/yxml.scala	Fri Jan 16 22:54:11 2009 +0100
@@ -109,12 +109,21 @@
       case _ => err("multiple results")
     }
 
+
+  /* failsafe parsing */
+
+  private def markup_failsafe(source: CharSequence) =
+    XML.Elem (Markup.BAD, Nil,
+      List(XML.Text(source.toString.replace(X_string, "\\<^X>").replace(Y_string, "\\<^Y>"))))
+
+  def parse_body_failsafe(source: CharSequence) = {
+    try { parse_body(source) }
+    catch { case _: RuntimeException => List(markup_failsafe(source)) }
+  }
+
   def parse_failsafe(source: CharSequence) = {
     try { parse(source) }
-    catch {
-      case _: RuntimeException => XML.Elem (Markup.BAD, Nil,
-        List(XML.Text(source.toString.replace(X_string, "\\<^X>").replace(Y_string, "\\<^Y>"))))
-    }
+    catch { case _: RuntimeException => markup_failsafe(source) }
   }
 
 }