diff -r 4123fca23296 -r ef8c9b3d5355 src/Pure/PIDE/markup_tree.scala
--- a/src/Pure/PIDE/markup_tree.scala	Thu Mar 04 15:49:15 2021 +0100
+++ b/src/Pure/PIDE/markup_tree.scala	Thu Mar 04 15:52:08 2021 +0100
@@ -94,7 +94,7 @@
 
         case (elems, body) =>
           val (end_offset, subtrees) =
-             body.foldLeft((offset, Nil: List[Markup_Tree]))(make_trees)
+             body.foldLeft((offset, List.empty[Markup_Tree]))(make_trees)
           if (offset == end_offset) acc
           else {
             val range = Text.Range(offset, end_offset)
@@ -105,7 +105,7 @@
     }
 
   def from_XML(body: XML.Body): Markup_Tree =
-    merge_disjoint(body.foldLeft((0, Nil: List[Markup_Tree]))(make_trees)._2)
+    merge_disjoint(body.foldLeft((0, List.empty[Markup_Tree]))(make_trees)._2)
 }