# HG changeset patch
# User wenzelm
# Date 1710252689 -3600
# Node ID 510fe8c3d9b865f78acb3d1eb962cbd6804a680a
# Parent  ea335307d45efaaa321f2acd4079491e31cb3c9f
tuned signature: more operations;

diff -r ea335307d45e -r 510fe8c3d9b8 src/Pure/library.scala
--- 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 }
 }