author | wenzelm |
Thu, 12 May 2011 16:42:57 +0200 | |
changeset 42719 | a2e9872d5459 |
parent 42718 | d7b2625c1193 |
child 42720 | caa4f1279154 |
--- 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) }