| changeset 42719 | a2e9872d5459 |
| parent 40453 | a81346e57cef |
| child 43650 | f00da558b78e |
--- a/src/Pure/General/yxml.scala Thu May 12 16:28:46 2011 +0200 +++ b/src/Pure/General/yxml.scala Thu May 12 16:42:57 2011 +0200 @@ -121,7 +121,7 @@ } } } - stack match { + (stack: @unchecked) match { case List((Markup.Empty, body)) => body.toList case (Markup(name, _), _) :: _ => err_unbalanced(name) }