minor performance tuning;

--- a/src/Pure/PIDE/rendering.scala	Tue Jul 29 22:42:35 2025 +0200
+++ b/src/Pure/PIDE/rendering.scala	Tue Jul 29 22:45:09 2025 +0200
@@ -121,10 +121,11 @@
       seen_serials += i
       b
     }
-    for {
-      Text.Info(range, entries) <- results
-      (i, elem) <- entries if !seen(i)
-    } yield Text.Info(range, elem)
+    List.from(
+      for {
+        Text.Info(range, entries) <- results.iterator
+        (i, elem) <- entries.iterator if !seen(i)
+      } yield Text.Info(range, elem))
   }