src/Pure/Build/build_manager.scala

 
 
   /** 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) {
     private val log_name = "build-manager"
     private val diff_ext = "diff"

     private def read_gz(file: Path, ext: String): Option[(String, String)] =
       if (!File.is_gz(file.file_name) || file.drop_ext.get_ext != ext) None
       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))
-
-      Report.Data(log, diffs)
-    }
-
-    def write_diff(name: String, diff: String): Unit =
+      val component_diffs =
+        File.read_dir(dir).flatMap(name => read_gz(dir + Path.basic(name), diff_ext))
+
+      Report.Data(build_log, component_diffs)
+    }
+
+    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 =
         build_log_file.lines.last match {
           case End(status) => Status.valueOf(status)

 
             if (task.kind != User_Build.name && _state.get_finished(task.kind).nonEmpty) {
               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))
               }
 
               for {
                 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,
               Component.isabelle(isabelle_rev) :: extra_components, task.timeout, start_date)
           } match {

 
               par(text("Start: " + Build_Log.print_date(job.start_date))) ::
               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))
 
               par(text("Start: " + Build_Log.print_date(result.start_date) +
                 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
           }
         }
 
       def render_cancelled: XML.Body = render_page("Build cancelled")(
         List(frontend_link(paths.frontend_url(Page.HOME), text("Home"))))