# HG changeset patch
# User wenzelm
# Date 1710063648 -3600
# Node ID c052a35e6a4f23852f1f3f67bec9cf733308ec6d
# Parent  ba306bc7d2261a8988d62a78837ce293959de920
tuned signature;

diff -r ba306bc7d226 -r c052a35e6a4f src/Pure/Build/build_process.scala
--- a/src/Pure/Build/build_process.scala	Sun Mar 10 10:37:28 2024 +0100
+++ b/src/Pure/Build/build_process.scala	Sun Mar 10 10:40:48 2024 +0100
@@ -97,7 +97,7 @@
     def iterator: Iterator[Build_Job.Session_Context] =
       for (name <- graph.topological_order.iterator) yield apply(name)
 
-    def data: Map[String, Build_Job.Session_Context] =
+    def data: Library.Update.Data[Build_Job.Session_Context] =
       Map.from(for ((_, (session, _)) <- graph.iterator) yield session.name -> session)
 
     def make(new_graph: Sessions.Graph): Sessions =
@@ -214,9 +214,9 @@
       serial + 1
     }
 
-    type Pending = Map[String, Task]
-    type Running = Map[String, Job]
-    type Results = Map[String, Result]
+    type Pending = Library.Update.Data[Task]
+    type Running = Library.Update.Data[Job]
+    type Results = Library.Update.Data[Result]
   }
 
   sealed case class State(