--- 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(