changeset 43768 | d52ab827d62b |
parent 43767 | e0219ef7f84c |
child 43778 | ce9189450447 |
--- 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) } }