# HG changeset patch # User wenzelm # Date 1717704790 -7200 # Node ID 9f89b3c414602a7b391e78fb39b0e36eb47b85df # Parent 198fc882ec0f45752df2f8b2775d95eee391f8f3 clarified signature; diff -r 198fc882ec0f -r 9f89b3c41460 src/Pure/Build/build_manager.scala --- a/src/Pure/Build/build_manager.scala Thu Jun 06 22:03:20 2024 +0200 +++ b/src/Pure/Build/build_manager.scala Thu Jun 06 22:13:10 2024 +0200 @@ -138,8 +138,8 @@ serial + 1 } - type Pending = Library.Update.Data[Task] - type Running = Library.Update.Data[Job] + type Pending = Name.Data[Task] + type Running = Name.Data[Job] type Finished = Map[String, Result] } diff -r 198fc882ec0f -r 9f89b3c41460 src/Pure/Build/build_process.scala --- a/src/Pure/Build/build_process.scala Thu Jun 06 22:03:20 2024 +0200 +++ b/src/Pure/Build/build_process.scala Thu Jun 06 22:13:10 2024 +0200 @@ -97,7 +97,7 @@ def store_heap(name: String): Boolean = isabelle.Sessions.is_pure(name) || iterator.exists(_.ancestors.contains(name)) - def data: Library.Update.Data[Build_Job.Session_Context] = + def data: Name.Data[Build_Job.Session_Context] = Map.from(for ((_, (session, _)) <- graph.iterator) yield session.name -> session) def make(new_graph: Sessions.Graph): Sessions = @@ -217,9 +217,9 @@ serial + 1 } - type Pending = Library.Update.Data[Task] - type Running = Library.Update.Data[Job] - type Results = Library.Update.Data[Result] + type Pending = Name.Data[Task] + type Running = Name.Data[Job] + type Results = Name.Data[Result] } sealed case class State( diff -r 198fc882ec0f -r 9f89b3c41460 src/Pure/library.scala --- a/src/Pure/library.scala Thu Jun 06 22:03:20 2024 +0200 +++ b/src/Pure/library.scala Thu Jun 06 22:13:10 2024 +0200 @@ -288,13 +288,11 @@ /* data update */ 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] - def data[A <: Name.T](old_data: Data[A], updates: List[Op[A]]): Data[A] = + def data[A <: Name.T](old_data: Name.Data[A], updates: List[Op[A]]): Name.Data[A] = updates.foldLeft(old_data) { case (map, Delete(name)) => map - name case (map, Insert(item)) => map + (item.name -> item) @@ -302,7 +300,7 @@ val empty: Update = Update() - def make[A](a: Data[A], b: Data[A], kind: Int = 0): Update = + def make[A](a: Name.Data[A], b: Name.Data[A], kind: Int = 0): Update = if (a eq b) empty else { val delete = List.from(for ((x, y) <- a.iterator if !b.get(x).contains(y)) yield x) diff -r 198fc882ec0f -r 9f89b3c41460 src/Pure/name.scala --- a/src/Pure/name.scala Thu Jun 06 22:03:20 2024 +0200 +++ b/src/Pure/name.scala Thu Jun 06 22:13:10 2024 +0200 @@ -9,4 +9,6 @@ object Name { trait T { def name: String } + + type Data[A] = Map[String, A] }