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