# HG changeset patch
# User wenzelm
# Date 1710010628 -3600
# Node ID c69ae2b8987e4b11ee9cc067963ec5c1c9f8daa2
# Parent  866d96915388cb6d483847242d4ba49c940f01d1
clarified signature: improved data integrity;

diff -r 866d96915388 -r c69ae2b8987e src/Pure/library.scala
--- a/src/Pure/library.scala	Sat Mar 09 17:23:09 2024 +0100
+++ b/src/Pure/library.scala	Sat Mar 09 19:57:08 2024 +0100
@@ -297,19 +297,18 @@
       else {
         val delete = List.from(for ((x, y) <- data0.iterator if !data1.get(x).contains(y)) yield x)
         val insert = List.from(for ((x, y) <- data1.iterator if !data0.get(x).contains(y)) yield x)
-        val domain = delete.toSet ++ insert
-        Update(domain = domain, delete = delete, insert = insert)
+        Update(delete = delete, insert = insert)
       }
   }
 
   sealed case class Update(
-    domain: Set[String] = Set.empty,
     delete: List[String] = Nil,
     insert: List[String] = Nil
   ) {
     def deletes: Boolean = delete.nonEmpty
     def inserts: Boolean = insert.nonEmpty
     def defined: Boolean = deletes || inserts
+    lazy val domain: Set[String] = delete.toSet ++ insert
   }