--- 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)