# HG changeset patch
# User wenzelm
# Date 1717703316 -7200
# Node ID 1d43005063384bbd3759a8012d5a1dd2ab36457c
# Parent  0428c7ad25aa9088a08f7db217f63bbaebbfaaf6
clarified signature;

diff -r 0428c7ad25aa -r 1d4300506338 etc/build.props
--- a/etc/build.props	Thu Jun 06 21:13:51 2024 +0200
+++ b/etc/build.props	Thu Jun 06 21:48:36 2024 +0200
@@ -238,6 +238,7 @@
   src/Pure/Tools/update_then.scala \
   src/Pure/Tools/update_theorems.scala \
   src/Pure/library.scala \
+  src/Pure/name.scala \
   src/Pure/pure_thy.scala \
   src/Pure/term.scala \
   src/Pure/term_xml.scala \
diff -r 0428c7ad25aa -r 1d4300506338 src/Pure/Build/build_job.scala
--- a/src/Pure/Build/build_job.scala	Thu Jun 06 21:13:51 2024 +0200
+++ b/src/Pure/Build/build_job.scala	Thu Jun 06 21:48:36 2024 +0200
@@ -99,7 +99,7 @@
     old_time: Time,
     old_command_timings_blob: Bytes,
     build_uuid: String
-  ) extends Library.Named
+  ) extends Name.T
 
   class Session_Job private[Build_Job](
     build_context: Build.Context,
diff -r 0428c7ad25aa -r 1d4300506338 src/Pure/Build/build_manager.scala
--- a/src/Pure/Build/build_manager.scala	Thu Jun 06 21:13:51 2024 +0200
+++ b/src/Pure/Build/build_manager.scala	Thu Jun 06 21:48:36 2024 +0200
@@ -88,7 +88,7 @@
 
   enum Priority { case low, normal, high }
 
-  sealed trait T extends Library.Named
+  sealed trait T extends Name.T
 
   sealed case class Task(
     build_config: Build_Config,
diff -r 0428c7ad25aa -r 1d4300506338 src/Pure/Build/build_process.scala
--- a/src/Pure/Build/build_process.scala	Thu Jun 06 21:13:51 2024 +0200
+++ b/src/Pure/Build/build_process.scala	Thu Jun 06 21:48:36 2024 +0200
@@ -52,7 +52,7 @@
     name: String,
     deps: List[String],
     build_uuid: String
-  ) extends Library.Named {
+  ) extends Name.T {
     def is_ready: Boolean = deps.isEmpty
     def resolve(dep: String): Option[Task] =
       if (deps.contains(dep)) Some(copy(deps = deps.filterNot(_ == dep))) else None
@@ -65,7 +65,7 @@
     node_info: Host.Node_Info,
     start_date: Date,
     build: Option[Build_Job]
-  ) extends Library.Named
+  ) extends Name.T
 
   sealed case class Result(
     name: String,
@@ -76,7 +76,7 @@
     process_result: Process_Result,
     output_shasum: SHA1.Shasum,
     current: Boolean
-  ) extends Library.Named {
+  ) extends Name.T {
     def ok: Boolean = process_result.ok
   }
 
diff -r 0428c7ad25aa -r 1d4300506338 src/Pure/library.scala
--- a/src/Pure/library.scala	Thu Jun 06 21:13:51 2024 +0200
+++ b/src/Pure/library.scala	Thu Jun 06 21:48:36 2024 +0200
@@ -285,11 +285,6 @@
     }
 
 
-  /* named items */
-
-  trait Named { def name: String }
-
-
   /* data update */
 
   object Update {
@@ -299,7 +294,7 @@
     case class Delete[A](name: String) extends Op[A]
     case class Insert[A](item: A) extends Op[A]
 
-    def data[A <: Named](old_data: Data[A], updates: List[Op[A]]): Data[A] =
+    def data[A <: Name.T](old_data: Data[A], updates: List[Op[A]]): Data[A] =
       updates.foldLeft(old_data) {
         case (map, Delete(name)) => map - name
         case (map, Insert(item)) => map + (item.name -> item)
diff -r 0428c7ad25aa -r 1d4300506338 src/Pure/name.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/name.scala	Thu Jun 06 21:48:36 2024 +0200
@@ -0,0 +1,12 @@
+/*  Title:      Pure/name.scala
+    Author:     Makarius
+
+Items with formal name.
+*/
+
+package isabelle
+
+
+object Name {
+  trait T { def name: String }
+}