# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1718030236 -7200
# Node ID 7b948ca986ec03b3dd84d305e21c74be3e432ae8
# Parent  5a6cc89c8f9806c681cd26173f0417b914b5799d
clarified;

diff -r 5a6cc89c8f98 -r 7b948ca986ec src/Pure/Build/build_manager.scala
--- a/src/Pure/Build/build_manager.scala	Mon Jun 10 16:14:44 2024 +0200
+++ b/src/Pure/Build/build_manager.scala	Mon Jun 10 16:37:16 2024 +0200
@@ -94,7 +94,11 @@
 
   enum Priority { case low, normal, high }
 
-  sealed trait T extends Name.T
+  object Build {
+    def name(kind: String, id: Long): String = kind + "/" + id
+  }
+  
+  sealed trait Build extends Name.T
 
   sealed case class Task(
     build_config: Build_Config,
@@ -103,7 +107,7 @@
     submit_date: Date = Date.now(),
     priority: Priority = Priority.normal,
     isabelle_rev: String = ""
-  ) extends T {
+  ) extends Build {
     def name: String = uuid.toString
     def kind: String = build_config.name
     def components: List[Component] = build_config.components
@@ -123,7 +127,7 @@
     components: List[Component],
     start_date: Date = Date.now(),
     cancelled: Boolean = false
-  ) extends T { def name: String = kind + "/" + id }
+  ) extends Build { def name: String = Build.name(kind, id) }
 
   object Status {
     def from_result(result: Process_Result): Status = {
@@ -142,7 +146,7 @@
     uuid: Option[UUID.T] = None,
     date: Date = Date.now(),
     serial: Long = 0,
-  ) extends T { def name: String = kind + "/" + id }
+  ) extends Build { def name: String = Build.name(kind, id) }
 
   object State {
     def max_serial(serials: Iterable[Long]): Long = serials.maxOption.getOrElse(0L)
@@ -207,10 +211,10 @@
     def get_finished(kind: String): List[Result] =
       (for ((_, result) <- finished if result.kind == kind) yield result).toList
 
-    def get(name: String): Option[T] =
+    def get(name: String): Option[Build] =
       pending.get(name).orElse(running.get(name)).orElse(finished.get(name))
 
-    def get(uuid: UUID.T): Option[T] =
+    def get(uuid: UUID.T): Option[Build] =
       pending.values.find(_.uuid == uuid).orElse(
         running.values.find(_.uuid == uuid)).orElse(
         finished.values.find(_.uuid.contains(uuid)))
@@ -878,22 +882,23 @@
     }
 
     class Cache private(keep: Time = Time.minutes(1)) {
-      var logs: Map[String, (Time, String)] = Map.empty
+      private var logs: Map[(String, Long), (Time, String)] = Map.empty
 
       def update(store: Store, state: State): Unit = synchronized {
         logs =
           for {
-            (name, (time, log)) <- logs
+            ((kind, id), (time, log)) <- logs
             if time + keep > Time.now()
-          } yield name -> (time, File.read(store.log_file(name)))
+          } yield (kind, id) -> (time, File.read(store.log_file(kind, id)))
       }
 
-      def lookup(store: Store, name: String): String = synchronized {
+      def lookup(store: Store, kind: String, id: Long): String = synchronized {
+        val name = (kind, id)
         logs.get(name) match {
           case Some((_, log)) =>
             logs += name -> (Time.now(), log)
           case None =>
-            logs += name -> (Time.now(), File.read(store.log_file(name)))
+            logs += name -> (Time.now(), File.read(store.log_file(kind, id)))
         }
         logs(name)._2
       }
@@ -912,7 +917,7 @@
       case Cancelled extends Model
       case Home(state: State) extends Model
       case Overview(kind: String, state: State) extends Model
-      case Build(elem: T, state: State, public: Boolean = true) extends Model
+      case Details(build: Build, state: State, public: Boolean = true) extends Model
     }
 
     object View {
@@ -998,8 +1003,8 @@
 
       private val ID = Params.key(Markup.ID)
 
-      def render_build(elem: T, state: State, public: Boolean): XML.Body =
-        render_page("Build: " + elem.name) {
+      def render_details(build: Build, state: State, public: Boolean): XML.Body =
+        render_page("Build: " + build.name) {
           def render_cancel(uuid: UUID.T): XML.Body =
             render_if(!public, List(
               submit_form("", List(hidden(ID, uuid.toString),
@@ -1011,7 +1016,7 @@
               if component.rev.nonEmpty
             } yield par(text(component.toString))
 
-          elem match {
+          build match {
             case task: Task =>
               par(text("Task from " + task.submit_date + ". ")) ::
               render_rev(task.isabelle_rev, task.components) :::
@@ -1022,11 +1027,11 @@
                 if (job.cancelled) text("Cancelling...")
                 else text("Running...") ::: render_cancel(job.uuid)) ::
               render_rev(job.isabelle_rev, job.components) :::
-              source(cache.lookup(store, job.name)) :: Nil
+              source(cache.lookup(store, job.kind, job.id)) :: Nil
             case result: Result =>
               par(text("Date: " + result.date)) ::
               par(text("Status: " + result.status)) ::
-              source(cache.lookup(store, result.name)) :: Nil
+              source(cache.lookup(store, result.kind, result.id)) :: Nil
           }
         }
 
@@ -1051,14 +1056,14 @@
           case _ => None
         }
 
-      def get_build(props: Properties.T): Option[Model.Build] =
+      def get_build(props: Properties.T): Option[Model.Details] =
         props match {
           case Markup.Name(name) =>
             val state = _state
-            state.get(name).map(Model.Build(_, state))
+            state.get(name).map(Model.Details(_, state))
           case Web_Server.Id(UUID(uuid)) =>
             val state = _state
-            state.get(uuid).map(Model.Build(_, state, public = false))
+            state.get(uuid).map(Model.Details(_, state, public = false))
           case _ => None
         }
 
@@ -1076,8 +1081,8 @@
                   _state = _state
                     .remove_running(job.name)
                     .add_running(job1)
-                  Model.Build(job1, _state, public = false)
-                case result: Result => Model.Build(result, _state, public = false)
+                  Model.Details(job1, _state, public = false)
+                case result: Result => Model.Details(result, _state, public = false)
               }
             }
         } yield model
@@ -1088,7 +1093,7 @@
             case Model.Error => HTML.text("invalid request")
             case Model.Home(state) => View.render_home(state)
             case Model.Overview(kind, state) => View.render_overview(kind, state)
-            case Model.Build(elem, state, public) => View.render_build(elem, state, public)
+            case Model.Details(build, state, public) => View.render_details(build, state, public)
             case Model.Cancelled => View.render_cancelled
           })
 
@@ -1118,12 +1123,12 @@
   /* context */
 
   case class Context(store: Store, task: Task, id: Long) {
-    def name = task.kind + "/" + id
-    def progress: Progress = new File_Progress(store.log_file(name))
+    def name = Build.name(task.kind, id)
+    def progress: Progress = new File_Progress(store.log_file(task.kind, id))
 
     def task_dir: Path = store.task_dir(task)
 
-    def init(): Unit = Isabelle_System.make_directory(store.log_file(name).dir)
+    def init(): Unit = Isabelle_System.make_directory(store.log_file(task.kind, id).dir)
 
     def isabelle_identifier: String =
       if (task.build_cluster) store.options.string("build_cluster_identifier") else store.identifier
@@ -1212,7 +1217,7 @@
     val finished = base_dir + Path.basic("finished")
 
     def task_dir(task: Task) = pending + Path.basic(task.uuid.toString)
-    def log_file(name: String): Path = finished + Path.explode(name)
+    def log_file(kind: String, id: Long): Path = finished + Path.make(List(kind, id.toString))
 
     def sync_permissions(dir: Path, ssh: SSH.System = SSH.Local): Unit = {
       ssh.execute("chmod -R g+rwx " + File.bash_path(dir))