# 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 } }