more precise exceptions;
authorwenzelm
Tue Jul 12 11:16:56 2011 +0200 (2011-07-12)
changeset 43768d52ab827d62b
parent 43767 e0219ef7f84c
child 43769 beba1a87caaa
more precise exceptions;
src/Pure/General/xml.ML
src/Pure/General/xml.scala
     1.1 --- a/src/Pure/General/xml.ML	Tue Jul 12 10:44:30 2011 +0200
     1.2 +++ b/src/Pure/General/xml.ML	Tue Jul 12 11:16:56 2011 +0200
     1.3 @@ -324,7 +324,11 @@
     1.4    | option f [t] = SOME (f (node t))
     1.5    | option _ ts = raise XML_BODY ts;
     1.6  
     1.7 -fun variant fs [t] = uncurry (nth fs) (tagged t)
     1.8 +fun variant fs [t] =
     1.9 +      let
    1.10 +        val (tag, ts) = tagged t;
    1.11 +        val f = nth fs tag handle General.Subscript => raise XML_BODY [t];
    1.12 +      in f ts end
    1.13    | variant _ ts = raise XML_BODY ts;
    1.14  
    1.15  end;
     2.1 --- a/src/Pure/General/xml.scala	Tue Jul 12 10:44:30 2011 +0200
     2.2 +++ b/src/Pure/General/xml.scala	Tue Jul 12 11:16:56 2011 +0200
     2.3 @@ -361,7 +361,10 @@
     2.4      {
     2.5        case List(t) =>
     2.6          val (tag, ts) = tagged(t)
     2.7 -        fs(tag)(ts)
     2.8 +        val f =
     2.9 +          try { fs(tag) }
    2.10 +          catch { case _: IndexOutOfBoundsException => throw new XML_Body(List(t)) }
    2.11 +        f(ts)
    2.12        case ts => throw new XML_Body(ts)
    2.13      }
    2.14    }