--- a/src/Pure/library.scala Thu Jun 06 21:13:51 2024 +0200
+++ b/src/Pure/library.scala Thu Jun 06 21:48:36 2024 +0200
@@ -285,11 +285,6 @@
}
- /* named items */
-
- trait Named { def name: String }
-
-
/* data update */
object Update {
@@ -299,7 +294,7 @@
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] =
+ def data[A <: Name.T](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)