# HG changeset patch
# User wenzelm
# Date 1710245845 -3600
# Node ID ea335307d45efaaa321f2acd4079491e31cb3c9f
# Parent  ede8b298cfe89cef3b3f0180e9cde3b5c0ed48a8
clarified signature: more explicit types;

diff -r ede8b298cfe8 -r ea335307d45e src/Pure/Build/build_process.scala
--- a/src/Pure/Build/build_process.scala	Tue Mar 12 11:18:38 2024 +0100
+++ b/src/Pure/Build/build_process.scala	Tue Mar 12 13:17:25 2024 +0100
@@ -388,7 +388,7 @@
       build_id: Long,
       serial_seen: Long,
       get: SQL.Result => A
-    ): List[(String, Option[A])] = {
+    ): List[Library.Update.Op[A]] = {
       val domain_columns = List(Updates.dom_name)
       val domain_table =
         SQL.Table("domain", domain_columns, body =
@@ -405,12 +405,10 @@
           domain_table.query_named + SQL.join_outer + table +
             " ON " + Updates.dom + " = " + Generic.name)
 
-      db.execute_query_statement(select_sql, List.from[(String, Option[A])],
-        { res =>
-          val delete = res.bool(Updates.delete)
-          val name = res.string(Updates.name)
-          if (delete) name -> None else name -> Some(get(res))
-        })
+      db.execute_query_statement(select_sql, List.from[Library.Update.Op[A]],
+        res =>
+          if (res.bool(Updates.delete)) Library.Update.Delete(res.string(Updates.name))
+          else Library.Update.Insert(get(res)))
     }
 
     def write_updates(
diff -r ede8b298cfe8 -r ea335307d45e src/Pure/library.scala
--- a/src/Pure/library.scala	Tue Mar 12 11:18:38 2024 +0100
+++ b/src/Pure/library.scala	Tue Mar 12 13:17:25 2024 +0100
@@ -290,6 +290,10 @@
   object Update {
     type Data[A] = Map[String, A]
 
+    sealed abstract class Op[A]
+    case class Delete[A](name: String) extends Op[A]
+    case class Insert[A](item: A) extends Op[A]
+
     val empty: Update = Update()
 
     def make[A](a: Data[A], b: Data[A], kind: Int = 0): Update =