--- a/src/Pure/library.scala Tue Mar 12 13:17:25 2024 +0100
+++ b/src/Pure/library.scala Tue Mar 12 15:11:29 2024 +0100
@@ -285,6 +285,11 @@
}
+ /* named items */
+
+ trait Named { def name: String }
+
+
/* data update */
object Update {
@@ -294,6 +299,12 @@
case class Delete[A](name: String) extends Op[A]
case class Insert[A](item: A) extends Op[A]
+ def data[A <: Named](old_data: Data[A], updates: List[Op[A]]): Data[A] =
+ updates.foldLeft(old_data) {
+ case (map, Delete(name)) => map - name
+ case (map, Insert(item)) => map + (item.name -> item)
+ }
+
val empty: Update = Update()
def make[A](a: Data[A], b: Data[A], kind: Int = 0): Update =
@@ -347,9 +358,4 @@
def as_subclass[C](c: Class[C])(x: AnyRef): Option[C] =
if (x == null || is_subclass(x.getClass, c)) Some(x.asInstanceOf[C]) else None
-
-
- /* named items */
-
- trait Named { def name: String }
}