src/Pure/PIDE/rendering.scala

--- a/src/Pure/PIDE/rendering.scala	Tue Aug 29 12:04:13 2023 +0200
+++ b/src/Pure/PIDE/rendering.scala	Tue Aug 29 12:53:28 2023 +0200
@@ -405,7 +405,7 @@
                 Some(snapshot.convert(info.range))
               else None)
         })
-    for (Text.Info(range, Some(range1)) <- result)
+    for (case Text.Info(range, Some(range1)) <- result)
       yield Text.Info(range, range1)
   }