diff -r dd86d35375a7 -r ee58db0396d8 src/Pure/Build/build_manager.scala --- a/src/Pure/Build/build_manager.scala Wed Jul 10 16:56:59 2024 +0200 +++ b/src/Pure/Build/build_manager.scala Wed Jul 10 16:58:39 2024 +0200 @@ -21,9 +21,10 @@ case _ => error("Malformed component: " + quote(s)) } + val Isabelle = "Isabelle" val AFP = "AFP" - def isabelle(rev: String = "") = Component("Isabelle", rev) + def isabelle(rev: String = "") = Component(Isabelle, rev) def afp(rev: String = "") = Component(AFP, rev) } @@ -873,9 +874,9 @@ val previous = _state.get_finished(task.kind).maxBy(_.id) for (isabelle_rev0 <- previous.isabelle_version) { - context.report.write_component_log("Isabelle", + context.report.write_component_log(Component.Isabelle, log(isabelle_repository, isabelle_rev0, isabelle_rev)) - context.report.write_component_diff("Isabelle", + context.report.write_component_diff(Component.Isabelle, diff(isabelle_repository, isabelle_rev0, isabelle_rev)) }