# HG changeset patch
# User wenzelm
# Date 1719583185 -7200
# Node ID 996b5eb7c89e38292ee4ae5a7b2ae0df2ed3ee80
# Parent  00f5e829d8b4420a0975e1526ef240f227fa8670
tuned;

diff -r 00f5e829d8b4 -r 996b5eb7c89e src/Pure/PIDE/xml.scala
--- a/src/Pure/PIDE/xml.scala	Fri Jun 28 13:25:51 2024 +0200
+++ b/src/Pure/PIDE/xml.scala	Fri Jun 28 15:59:45 2024 +0200
@@ -48,7 +48,7 @@
 
     def traverse(trees: List[Tree]): Unit = {
       @tailrec def trav(list: List[Trav]): Unit =
-        list match {
+        (list : @unchecked) match {
           case Nil =>
           case Text(s) :: rest => text(s); trav(rest)
           case Elem(markup, body) :: rest =>
@@ -56,7 +56,6 @@
             else if (body.isEmpty) { elem(markup, end = true); trav(rest) }
             else { elem(markup); trav(body ::: End(markup.name) :: rest) }
           case End(name) :: rest => end_elem(name); trav(rest)
-          case _ :: _ => ???
         }
       trav(trees)
     }