diff -r 5fdca5bfc0b4 -r 7d8e0e3c553b src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Tue May 14 16:54:47 2013 +0200
+++ b/src/Pure/PIDE/protocol.scala	Tue May 14 19:30:21 2013 +0200
@@ -21,8 +21,7 @@
       }
       catch {
         case ERROR(_) => None
-        case _: XML.XML_Atom => None
-        case _: XML.XML_Body => None
+        case _: XML.Error => None
       }
   }
 
@@ -35,8 +34,7 @@
       }
       catch {
         case ERROR(_) => None
-        case _: XML.XML_Atom => None
-        case _: XML.XML_Body => None
+        case _: XML.Error => None
       }
   }