# HG changeset patch
# User wenzelm
# Date 1678725043 -3600
# Node ID 89fffc5f5728d7e58d16adfb49c387ec716b976c
# Parent  86ef80d135447db290601e42780ce6fed2e8e3a1
tuned whitespace;

diff -r 86ef80d13544 -r 89fffc5f5728 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Mon Mar 13 17:22:43 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Mon Mar 13 17:30:43 2023 +0100
@@ -143,7 +143,23 @@
 
   type Progress_Messages = SortedMap[Long, Progress.Message]
 
-  case class Task(name: String, deps: List[String], info: JSON.Object.T = JSON.Object.empty) {
+  case class Worker(
+    worker_uuid: String,
+    build_uuid: String,
+    hostname: String,
+    java_pid: Long,
+    java_start: Date,
+    start: Date,
+    stamp: Date,
+    stop: Option[Date],
+    serial: Long
+  )
+
+  case class Task(
+    name: String,
+    deps: List[String],
+    info: JSON.Object.T = JSON.Object.empty
+  ) {
     def is_ready: Boolean = deps.isEmpty
     def resolve(dep: String): Task =
       if (deps.contains(dep)) copy(deps = deps.filterNot(_ == dep)) else this
@@ -158,17 +174,6 @@
     def no_build: Job = copy(build = None)
   }
 
-  case class Worker(
-    worker_uuid: String,
-    build_uuid: String,
-    hostname: String,
-    java_pid: Long,
-    java_start: Date,
-    start: Date,
-    stamp: Date,
-    stop: Option[Date],
-    serial: Long)
-
   case class Result(
     process_result: Process_Result,
     output_shasum: SHA1.Shasum,