# 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]
 }