# HG changeset patch
# User wenzelm
# Date 1368552621 -7200
# Node ID 7d8e0e3c553b308cf54fcefd3c8c98d0712bebdd
# Parent  5fdca5bfc0b4644fb2a96aced644fc52d7e485ea
tuned signature;

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
       }
   }
 
diff -r 5fdca5bfc0b4 -r 7d8e0e3c553b 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
   {
diff -r 5fdca5bfc0b4 -r 7d8e0e3c553b src/Pure/Thy/present.scala
--- a/src/Pure/Thy/present.scala	Tue May 14 16:54:47 2013 +0200
+++ b/src/Pure/Thy/present.scala	Tue May 14 19:30:21 2013 +0200
@@ -40,7 +40,7 @@
 
     val sessions0 =
       try { read_sessions(dir) }
-      catch { case _: XML.XML_Atom => Nil case _: XML.XML_Body => Nil }
+      catch { case _: XML.Error => Nil }
 
     val sessions = (SortedMap.empty[String, String] ++ sessions0 ++ new_sessions).toList
 
diff -r 5fdca5bfc0b4 -r 7d8e0e3c553b src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Tue May 14 16:54:47 2013 +0200
+++ b/src/Pure/Tools/build.scala	Tue May 14 19:30:21 2013 +0200
@@ -722,7 +722,7 @@
       catch {
         case ERROR(msg) => ignore_error(msg)
         case exn: java.lang.Error => ignore_error(Exn.message(exn))
-        case _: XML.XML_Atom | _: XML.XML_Body => ignore_error("")
+        case _: XML.Error => ignore_error("")
       }
     }