# HG changeset patch
# User wenzelm
# Date 1673731420 -3600
# Node ID 5ba8cb258e75eae3f42dad71e5b970b30d7ddbab
# Parent  4307b5de7009be4a0a2d44e2360675193f026e02
proper normal form of adjacent XML.Text, notably for Bibtex.update_cite;

diff -r 4307b5de7009 -r 5ba8cb258e75 src/Pure/PIDE/markup_tree.scala
--- a/src/Pure/PIDE/markup_tree.scala	Sat Jan 14 21:01:26 2023 +0100
+++ b/src/Pure/PIDE/markup_tree.scala	Sat Jan 14 22:23:40 2023 +0100
@@ -242,6 +242,16 @@
           else List(XML.Wrapped_Elem(elem.markup, elem.body, b))
       }
 
+    @tailrec def normal_body(trees: List[XML.Tree], res: XML.Body = Nil): XML.Body =
+      if (trees.isEmpty) res.reverse
+      else {
+        val (texts, trees1) = Library.take_prefix[XML.Tree](_.isInstanceOf[XML.Text], trees)
+        val (elems, trees2) = Library.take_prefix[XML.Tree](_.isInstanceOf[XML.Elem], trees1)
+        val res1 = XML.content(texts) match { case "" => res case txt => XML.Text(txt) :: res }
+        val res2 = elems.foldLeft(res1)({ case (ts, t) => t :: ts })
+        normal_body(trees2, res2)
+      }
+
     def make_body(
       elem_range: Text.Range,
       elem_markup: List[XML.Elem],
@@ -256,7 +266,7 @@
         last = subrange.stop
       }
       body ++= make_text(last, elem_range.stop)
-      make_elems(elem_markup, body.toList)
+      make_elems(elem_markup, normal_body(body.toList))
     }
     make_body(root_range, Nil, overlapping(root_range))
   }