tuned signature;
authorwenzelm
Sun, 10 Mar 2024 10:40:48 +0100
changeset 79843 c052a35e6a4f
parent 79842 ba306bc7d226
child 79844 ac40138234ce
tuned signature;
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(