# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1720623711 -7200
# Node ID 77c78910544cbd14e3f353d1ab17b08334448548
# Parent  ee58db0396d8982c329bf0a9de345a6ca4c11107
clarified;

diff -r ee58db0396d8 -r 77c78910544c src/Pure/Build/build_manager.scala
--- a/src/Pure/Build/build_manager.scala	Wed Jul 10 16:58:39 2024 +0200
+++ b/src/Pure/Build/build_manager.scala	Wed Jul 10 17:01:51 2024 +0200
@@ -636,11 +636,32 @@
       Report.Data(build_log, component_logs, 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 write_log(
+      component: String,
+      repository: Mercurial.Repository,
+      rev0: String,
+      rev: String
+    ): Unit =
+      if (rev0.nonEmpty && rev.nonEmpty && rev0 != rev) {
+        val log_opts = "--graph --color always"
+        val rev1 = "children(" + rev0 + ")"
+        val cmd = repository.command_line("log", Mercurial.opt_rev(rev1 + ":" + rev), log_opts)
+        val log = Isabelle_System.bash("export HGPLAINEXCEPT=color\n" + cmd).check.out
+        if (log.nonEmpty) File.write_gzip(dir + Path.basic(component).ext(log_ext).gz, log)
+      }
 
-    def write_component_log(name: String, log: String): Unit =
-      if (log.nonEmpty) File.write_gzip(dir + Path.basic(name).ext(log_ext).gz, log)
+    def write_diff(
+      component: String,
+      repository: Mercurial.Repository,
+      rev0: String,
+      rev: String
+    ): Unit =
+      if (rev0.nonEmpty && rev.nonEmpty) {
+        val diff_opts = "--noprefix --nodates --ignore-all-space --color always"
+        val cmd = repository.command_line("diff", Mercurial.opt_rev(rev0 + ":" + rev), diff_opts)
+        val diff = Isabelle_System.bash("export HGPLAINEXCEPT=color\n" + cmd).check.out
+        if (diff.nonEmpty) File.write_gzip(dir + Path.basic(component).ext(diff_ext).gz, diff)
+      }
 
     def result(uuid: Option[UUID.T]): Result = {
       val End = """^Job ended at [^,]+, with status (\w+)$""".r
@@ -802,23 +823,6 @@
       }
     }
 
-    private def diff(repository: Mercurial.Repository, rev0: String, rev: String): String =
-      if (rev0.isEmpty || rev.isEmpty) ""
-      else {
-        val diff_opts = "--noprefix --nodates --ignore-all-space --color always"
-        val cmd = repository.command_line("diff", Mercurial.opt_rev(rev0 + ":" + rev), diff_opts)
-        Isabelle_System.bash("export HGPLAINEXCEPT=color\n" + cmd).check.out
-      }
-
-    private def log(repository: Mercurial.Repository, rev0: String, rev: String): String =
-      if (rev0.isEmpty || rev.isEmpty || rev0 == rev) ""
-      else {
-        val log_opts = "--graph --color always"
-        val rev1 = "children(" + rev0 + ")"
-        val cmd = repository.command_line("log", Mercurial.opt_rev(rev1 + ":" + rev), log_opts)
-        Isabelle_System.bash("export HGPLAINEXCEPT=color\n" + cmd).check.out
-      }
-
     private def start_next(): Option[Context] =
       synchronized_database("start_next") {
         for ((name, task) <- _state.pending if Exn.is_exn(Exn.capture(task.build_hosts))) {
@@ -874,10 +878,10 @@
               val previous = _state.get_finished(task.kind).maxBy(_.id)
 
               for (isabelle_rev0 <- previous.isabelle_version) {
-                context.report.write_component_log(Component.Isabelle,
-                  log(isabelle_repository, isabelle_rev0, isabelle_rev))
-                context.report.write_component_diff(Component.Isabelle,
-                  diff(isabelle_repository, isabelle_rev0, isabelle_rev))
+                context.report.write_log(Component.Isabelle,
+                  isabelle_repository, isabelle_rev0, isabelle_rev)
+                context.report.write_diff(Component.Isabelle,
+                  isabelle_repository, isabelle_rev0, isabelle_rev)
               }
 
               for {
@@ -885,8 +889,8 @@
                 afp <- extra_components.find(_.name == Component.AFP)
                 sync_dir <- sync_dirs.find(_.name == afp.name)
               } {
-                context.report.write_component_log(afp.name, log(sync_dir.hg, afp_rev0, afp.rev))
-                context.report.write_component_diff(afp.name, diff(sync_dir.hg, afp_rev0, afp.rev))
+                context.report.write_log(afp.name, sync_dir.hg, afp_rev0, afp.rev)
+                context.report.write_diff(afp.name, sync_dir.hg, afp_rev0, afp.rev)
               }
             }