tuned;

--- a/src/Pure/PIDE/markup_tree.scala	Wed Dec 02 15:01:37 2020 +0100
+++ b/src/Pure/PIDE/markup_tree.scala	Sat Dec 05 11:49:04 2020 +0100
@@ -58,7 +58,7 @@
       var result: List[XML.Elem] = Nil
       for (elem <- rev_markup if elements(elem.name))
         result ::= elem
-      result.toList
+      result
     }
 
     def + (markup: Text.Markup): Entry = copy(rev_markup = markup.info :: rev_markup)