diff -r 131f7ea9e6e6 -r 6dd90ef9f927 src/Pure/General/yxml.scala
--- a/src/Pure/General/yxml.scala	Mon Aug 25 16:52:11 2008 +0200
+++ b/src/Pure/General/yxml.scala	Mon Aug 25 20:01:17 2008 +0200
@@ -49,9 +49,7 @@
 
   /* parsing */
 
-  class BadYXML(msg: String) extends Exception
-
-  private def err(msg: String) = throw new BadYXML(msg)
+  private def err(msg: String) = error("Malformed YXML: " + msg)
   private def err_attribute() = err("bad attribute")
   private def err_element() = err("bad element")
   private def err_unbalanced(name: String) =
@@ -115,7 +113,7 @@
   def parse_failsafe(source: CharSequence) = {
     try { parse(source) }
     catch {
-      case e: BadYXML => XML.Elem (Markup.BAD, Nil,
+      case _: RuntimeException => XML.Elem (Markup.BAD, Nil,
         List(XML.Text(source.toString.replace(X_string, "\\<^X>").replace(Y_string, "\\<^Y>"))))
     }
   }