# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1720516809 -7200
# Node ID d5ff748321b7a94daf37b1b841c729c5b3b1868d
# Parent  c54a4c2db5b7d419423213e0dd254b612046b4c1
clarified names;

diff -r c54a4c2db5b7 -r d5ff748321b7 src/Pure/Build/build_manager.scala
--- a/src/Pure/Build/build_manager.scala	Tue Jul 09 11:11:15 2024 +0200
+++ b/src/Pure/Build/build_manager.scala	Tue Jul 09 11:20:09 2024 +0200
@@ -599,7 +599,7 @@
   /** build reports **/
 
   object Report {
-    case class Data(log: String, diffs: List[(String, String)])
+    case class Data(build_log: String, component_diffs: List[(String, String)])
   }
 
   case class Report(kind: String, id: Long, dir: Path) {
@@ -620,21 +620,22 @@
       else Some(file.drop_ext.drop_ext.file_name -> File.read_gzip(file))
 
     def read: Report.Data = {
-      val log =
+      val build_log =
         if_proper(ok, if (log_file.is_file) File.read(log_file) else File.read_gzip(log_file_gz))
 
-      val diffs = File.read_dir(dir).flatMap(name => read_gz(dir + Path.basic(name), diff_ext))
+      val component_diffs =
+        File.read_dir(dir).flatMap(name => read_gz(dir + Path.basic(name), diff_ext))
 
-      Report.Data(log, diffs)
+      Report.Data(build_log, component_diffs)
     }
 
-    def write_diff(name: String, diff: String): Unit =
+    def write_component_diff(name: String, diff: String): Unit =
       if (diff.nonEmpty) File.write_gzip(dir + Path.basic(name).ext(diff_ext).gz, diff)
 
     def result(uuid: Option[UUID.T]): Result = {
       val End = """^Job ended at [^,]+, with status (\w+)$""".r
 
-      val build_log_file = Build_Log.Log_File(log_name, Library.trim_split_lines(read.log))
+      val build_log_file = Build_Log.Log_File(log_name, Library.trim_split_lines(read.build_log))
 
       val meta_info = build_log_file.parse_meta_info()
       val status =
@@ -854,7 +855,7 @@
               val previous = _state.get_finished(task.kind).maxBy(_.id)
 
               for (isabelle_rev0 <- previous.isabelle_version) {
-                context.report.write_diff("Isabelle",
+                context.report.write_component_diff("Isabelle",
                   diff(isabelle_repository, isabelle_rev0, isabelle_rev))
               }
 
@@ -862,7 +863,7 @@
                 afp_rev0 <- previous.afp_version
                 afp <- extra_components.find(_.name == Component.AFP)
                 sync_dir <- sync_dirs.find(_.name == afp.name)
-              } context.report.write_diff(afp.name, diff(sync_dir.hg, afp_rev0, afp.rev))
+              } context.report.write_component_diff(afp.name, diff(sync_dir.hg, afp_rev0, afp.rev))
             }
 
             Job(task.uuid, task.kind, id, task.build_cluster, hostnames,
@@ -1230,8 +1231,8 @@
               par(
                 if (job.cancelled) text("Cancelling ...")
                 else text("Running ...") ::: render_cancel(job.uuid)) ::
-              render_rev(job.components, report_data.diffs.toMap) :::
-              par(text("Log") :+ source(report_data.log)) :: Nil
+              render_rev(job.components, report_data.component_diffs.toMap) :::
+              par(text("Log") :+ source(report_data.build_log)) :: Nil
 
             case result: Result =>
               val report_data = cache.lookup(store.report(result.kind, result.id))
@@ -1240,8 +1241,8 @@
                 if_proper(result.end_date,
                   ", took " + (result.end_date.get - result.start_date).message_hms))) ::
               par(text("Status: " + result.status)) ::
-              render_rev(result.components, report_data.diffs.toMap) :::
-              par(text("Log") :+ source(report_data.log)) :: Nil
+              render_rev(result.components, report_data.component_diffs.toMap) :::
+              par(text("Log") :+ source(report_data.build_log)) :: Nil
           }
         }