diff -r b1e0fb71435d -r fdfe9b91d96e src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Tue Aug 29 12:04:13 2023 +0200
+++ b/src/Pure/PIDE/document.scala	Tue Aug 29 12:53:28 2023 +0200
@@ -785,7 +785,7 @@
             case some => Some(some)
           }
       }
-      for (Text.Info(r, Some(x)) <- cumulate(range, None, elements, result1, status))
+      for (case Text.Info(r, Some(x)) <- cumulate(range, None, elements, result1, status))
         yield Text.Info(r, x)
     }
   }
@@ -1262,7 +1262,7 @@
       val pending_edits1 =
         (for {
           change <- history.undo_list.takeWhile(_ != stable)
-          (name, Node.Edits(es)) <- change.rev_edits
+          case (name, Node.Edits(es)) <- change.rev_edits
         } yield (name -> es)).foldLeft(pending_edits)(_ + _)
 
       new Snapshot(this, version, node_name, pending_edits1, snippet_command)