# HG changeset patch
# User wenzelm
# Date 1688222872 -7200
# Node ID 8c0d3c879f7cc48515c22f88d2e2f9dbca3739d7
# Parent  c2c59de57df99707c3edfd30426a6e6e032c9403
tuned signature;

diff -r c2c59de57df9 -r 8c0d3c879f7c src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Sat Jul 01 16:42:57 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Sat Jul 01 16:47:52 2023 +0200
@@ -45,7 +45,7 @@
 
   /** dynamic state **/
 
-  case class Build(
+  sealed case class Build(
     build_uuid: String,   // Database_Progress.context_uuid
     ml_platform: String,
     options: String,
@@ -56,7 +56,7 @@
     def active: Boolean = stop.isEmpty
   }
 
-  case class Worker(
+  sealed case class Worker(
     worker_uuid: String,  // Database_Progress.agent_uuid
     build_uuid: String,
     start: Date,
@@ -65,7 +65,7 @@
     serial: Long
   )
 
-  case class Task(
+  sealed case class Task(
     name: String,
     deps: List[String],
     info: JSON.Object.T,
@@ -76,7 +76,7 @@
       if (deps.contains(dep)) copy(deps = deps.filterNot(_ == dep)) else this
   }
 
-  case class Job(
+  sealed case class Job(
     name: String,
     worker_uuid: String,
     build_uuid: String,
@@ -86,7 +86,7 @@
     def no_build: Job = copy(build = None)
   }
 
-  case class Result(
+  sealed case class Result(
     name: String,
     worker_uuid: String,
     build_uuid: String,