src/Pure/PIDE/xml.scala

--- a/src/Pure/PIDE/xml.scala	Tue May 14 16:54:47 2013 +0200
+++ b/src/Pure/PIDE/xml.scala	Tue May 14 19:30:21 2013 +0200
@@ -199,8 +199,9 @@
 
   /** XML as data representation language **/
 
-  class XML_Atom(s: String) extends Exception(s)
-  class XML_Body(body: XML.Body) extends Exception
+  abstract class Error(s: String) extends Exception(s)
+  class XML_Atom(s: String) extends Error(s)
+  class XML_Body(body: XML.Body) extends Error("")
 
   object Encode
   {