# HG changeset patch
# User wenzelm
# Date 1719658243 -7200
# Node ID 99e276c441215b6502f18fae8e75ac4e04f41294
# Parent  1b5ba70a64b9f85dc1ceddf4f96edd265665b210
minor performance tuning;

diff -r 1b5ba70a64b9 -r 99e276c44121 src/Pure/PIDE/protocol_message.scala
--- a/src/Pure/PIDE/protocol_message.scala	Sat Jun 29 12:42:47 2024 +0200
+++ b/src/Pure/PIDE/protocol_message.scala	Sat Jun 29 12:50:43 2024 +0200
@@ -64,7 +64,7 @@
         List(XML.Wrapped_Elem(Markup(Markup.REPORT, props ::: ps), body, ts))
       case XML.Elem(Markup(Markup.REPORT, ps), ts) =>
         List(XML.Elem(Markup(Markup.REPORT, props ::: ps), ts))
-      case XML.Wrapped_Elem(_, _, ts) => reports(props, ts)
+      case XML.Wrapped_Elem_Body(ts) => reports(props, ts)
       case XML.Elem(_, ts) => reports(props, ts)
       case XML.Text(_) => Nil
     }
diff -r 1b5ba70a64b9 -r 99e276c44121 src/Pure/PIDE/xml.scala
--- a/src/Pure/PIDE/xml.scala	Sat Jun 29 12:42:47 2024 +0200
+++ b/src/Pure/PIDE/xml.scala	Sat Jun 29 12:50:43 2024 +0200
@@ -118,6 +118,17 @@
       }
   }
 
+  object Wrapped_Elem_Body {
+    def unapply(tree: Tree): Option[Body] =
+      tree match {
+        case
+          XML.Elem(Markup(XML_ELEM, (XML_NAME, _) :: _),
+            XML.Elem(Markup(XML_BODY, Nil), _) :: body) =>
+          Some(body)
+        case _ => None
+      }
+  }
+
   object Root_Elem {
     def apply(body: Body): XML.Elem = XML.Elem(Markup(XML_ELEM, Nil), body)
     def unapply(tree: Tree): Option[Body] =
@@ -134,7 +145,7 @@
     @tailrec def trav(x: A, list: List[Tree]): A =
       list match {
         case Nil => x
-        case XML.Wrapped_Elem(_, _, body) :: rest => trav(x, body ::: rest)
+        case XML.Wrapped_Elem_Body(body) :: rest => trav(x, body ::: rest)
         case XML.Elem(_, body) :: rest => trav(x, body ::: rest)
         case XML.Text(s) :: rest => trav(op(x, s), rest)
       }