tuned;
authorwenzelm
Sat, 05 Dec 2020 11:49:04 +0100
changeset 73051 85aaaf2cd173
parent 73050 51eec6d51882
child 73052 ea4f86914cb2
tuned;
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)