# HG changeset patch
# User wenzelm
# Date 1310462216 -7200
# Node ID d52ab827d62b80c2b847e0ca10c6c6ddf8db51e2
# Parent  e0219ef7f84c7dcf171e7d77dc2a0e9ff737b397
more precise exceptions;

diff -r e0219ef7f84c -r d52ab827d62b src/Pure/General/xml.ML
--- a/src/Pure/General/xml.ML	Tue Jul 12 10:44:30 2011 +0200
+++ b/src/Pure/General/xml.ML	Tue Jul 12 11:16:56 2011 +0200
@@ -324,7 +324,11 @@
   | option f [t] = SOME (f (node t))
   | option _ ts = raise XML_BODY ts;
 
-fun variant fs [t] = uncurry (nth fs) (tagged t)
+fun variant fs [t] =
+      let
+        val (tag, ts) = tagged t;
+        val f = nth fs tag handle General.Subscript => raise XML_BODY [t];
+      in f ts end
   | variant _ ts = raise XML_BODY ts;
 
 end;
diff -r e0219ef7f84c -r d52ab827d62b src/Pure/General/xml.scala
--- a/src/Pure/General/xml.scala	Tue Jul 12 10:44:30 2011 +0200
+++ b/src/Pure/General/xml.scala	Tue Jul 12 11:16:56 2011 +0200
@@ -361,7 +361,10 @@
     {
       case List(t) =>
         val (tag, ts) = tagged(t)
-        fs(tag)(ts)
+        val f =
+          try { fs(tag) }
+          catch { case _: IndexOutOfBoundsException => throw new XML_Body(List(t)) }
+        f(ts)
       case ts => throw new XML_Body(ts)
     }
   }