clarified;
authorFabian Huch <huch@in.tum.de>
Wed, 10 Jul 2024 16:58:39 +0200
changeset 80543 ee58db0396d8
parent 80542 dd86d35375a7
child 80544 77c78910544c
clarified;
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))
               }