# HG changeset patch
# User wenzelm
# Date 1607165344 -3600
# Node ID 85aaaf2cd1735be59cf305d6f3183f381a362a6e
# Parent  51eec6d518823e5b11757c7d6e7544fa4b3ac29e
tuned;

diff -r 51eec6d51882 -r 85aaaf2cd173 src/Pure/PIDE/markup_tree.scala
--- 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)