src/Pure/General/yxml.scala

--- a/src/Pure/General/yxml.scala	Sun Jul 03 19:53:35 2011 +0200
+++ b/src/Pure/General/yxml.scala	Mon Jul 04 13:43:10 2011 +0200
@@ -144,12 +144,12 @@
   def parse_body_failsafe(source: CharSequence): XML.Body =
   {
     try { parse_body(source) }
-    catch { case _: RuntimeException => List(markup_failsafe(source)) }
+    catch { case ERROR(_) => List(markup_failsafe(source)) }
   }
 
   def parse_failsafe(source: CharSequence): XML.Tree =
   {
     try { parse(source) }
-    catch { case _: RuntimeException => markup_failsafe(source) }
+    catch { case ERROR(_) => markup_failsafe(source) }
   }
 }