# HG changeset patch
# User wenzelm
# Date 1725918658 -7200
# Node ID aaf9e8a392cca081e4f21a4a3df557787d9267fe
# Parent  ddc062eac8712ec9766fa4189ad7afbf91d363d8
minor performance tuning, following Isabelle/Scala;

diff -r ddc062eac871 -r aaf9e8a392cc src/Pure/PIDE/xml.ML
--- a/src/Pure/PIDE/xml.ML	Mon Sep 09 23:47:08 2024 +0200
+++ b/src/Pure/PIDE/xml.ML	Mon Sep 09 23:50:58 2024 +0200
@@ -96,8 +96,8 @@
 (* text content *)
 
 fun add_content tree =
-  (case unwrap_elem tree of
-    SOME (_, ts) => fold add_content ts
+  (case unwrap_elem_body tree of
+    SOME ts => fold add_content ts
   | NONE =>
       (case tree of
         Elem (_, ts) => fold add_content ts
diff -r ddc062eac871 -r aaf9e8a392cc src/Pure/PIDE/xml_type.ML
--- a/src/Pure/PIDE/xml_type.ML	Mon Sep 09 23:47:08 2024 +0200
+++ b/src/Pure/PIDE/xml_type.ML	Mon Sep 09 23:50:58 2024 +0200
@@ -16,6 +16,7 @@
   val xml_bodyN: string
   val wrap_elem: ((string * attributes) * body) * body -> tree
   val unwrap_elem: tree -> (((string * attributes) * body) * body) option
+  val unwrap_elem_body: tree -> body option
   val content_of: body -> string
 end
 
@@ -45,14 +46,19 @@
       then SOME (((a, atts), body1), body2) else NONE
   | unwrap_elem _ = NONE;
 
+fun unwrap_elem_body (Elem ((name, (n, _) :: _), Elem ((name', []), _) :: body)) =
+      if name = xml_elemN andalso n = xml_nameN andalso name' = xml_bodyN
+      then SOME body else NONE
+  | unwrap_elem_body _ = NONE;
+
 
 (* text content *)
 
 fun add_contents [] res = res
   | add_contents (t :: ts) res = add_contents ts (add_content t res)
 and add_content tree res =
-  (case unwrap_elem tree of
-    SOME (_, ts) => add_contents ts res
+  (case unwrap_elem_body tree of
+    SOME ts => add_contents ts res
   | NONE =>
       (case tree of
         Elem (_, ts) => add_contents ts res