# HG changeset patch
# User wenzelm
# Date 1719657767 -7200
# Node ID 1b5ba70a64b9f85dc1ceddf4f96edd265665b210
# Parent  e0bd9e4811ad0c88edcf0fffdf6a5b179d21fc6a
minor performance tuning;

diff -r e0bd9e4811ad -r 1b5ba70a64b9 src/Pure/PIDE/xml.scala
--- a/src/Pure/PIDE/xml.scala	Fri Jun 28 23:53:48 2024 +0200
+++ b/src/Pure/PIDE/xml.scala	Sat Jun 29 12:42:47 2024 +0200
@@ -47,16 +47,24 @@
     def end_elem(name: String): Unit
 
     def traverse(trees: List[Tree]): Unit = {
+      @tailrec def trav_atomic(list: List[Trav]): List[Trav] =
+        list match {
+          case Text(s) :: rest => text(s); trav_atomic(rest)
+          case Elem(markup, Nil) :: rest =>
+            if (!markup.is_empty) elem(markup, end = true)
+            trav_atomic(rest)
+          case End(name) :: rest => end_elem(name); trav_atomic(rest)
+          case _ => list
+        }
+
       @tailrec def trav(list: List[Trav]): Unit =
-        (list : @unchecked) match {
+        (trav_atomic(list) : @unchecked) match {
           case Nil =>
-          case Text(s) :: rest => text(s); trav(rest)
-          case Elem(markup, body) :: rest =>
-            if (markup.is_empty) trav(body ::: rest)
-            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 Elem(markup, body) :: rest if body.nonEmpty =>
+            if (markup.is_empty) trav(trav_atomic(body) ::: rest)
+            else { elem(markup); trav(trav_atomic(body) ::: End(markup.name) :: rest) }
         }
+
       trav(trees)
     }
   }