# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1720623419 -7200
# Node ID dd86d35375a75ab94e9ca150dde51a82830563bd
# Parent  5ebfe18e39525a125fd65ef1b09c99745b62a148
log and display components with empty (unknown) revisions to indicate that they are present;

diff -r 5ebfe18e3952 -r dd86d35375a7 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Wed Jul 10 09:58:32 2024 +0200
+++ b/src/Pure/Admin/build_log.scala	Wed Jul 10 16:56:59 2024 +0200
@@ -349,8 +349,8 @@
     val engine = "build_manager"
     val Start = new Regex("""^Starting job \S+ at ([^,]+), on (\S+)$""")
     val End = new Regex("""^Job ended at ([^,]+), with status \w+$""")
-    val Isabelle_Version = List(new Regex("""^Using Isabelle/(\w+)$"""))
-    val AFP_Version = List(new Regex("""^Using AFP/(\w+)$"""))
+    val Isabelle_Version = List(new Regex("""^Using Isabelle/?(\w*)$"""))
+    val AFP_Version = List(new Regex("""^Using AFP/?(\w*)$"""))
   }
 
   private def parse_meta_info(log_file: Log_File): Meta_Info = {
diff -r 5ebfe18e3952 -r dd86d35375a7 src/Pure/Build/build_manager.scala
--- a/src/Pure/Build/build_manager.scala	Wed Jul 10 09:58:32 2024 +0200
+++ b/src/Pure/Build/build_manager.scala	Wed Jul 10 16:56:59 2024 +0200
@@ -28,7 +28,7 @@
   }
 
   case class Component(name: String, rev: String = "") {
-    override def toString: String = name + "/" + rev
+    override def toString: String = name + if_proper(rev, "/" + rev)
 
     def is_local: Boolean = rev.isEmpty
   }
@@ -895,7 +895,7 @@
             case Exn.Res(job) =>
               _state = _state.add_running(job)
 
-              for (component <- job.components if !component.is_local)
+              for (component <- job.components)
                 context.report.progress.echo("Using " + component.toString)
 
               Some(context)
@@ -1219,22 +1219,18 @@
               submit_form("", List(hidden(ID, uuid.toString),
                 api_button(paths.api_route(API.BUILD_CANCEL), "cancel build")))))
 
-          def non_local(components: List[Component]): List[Component] =
-            for (component <- components if !component.is_local) yield component
+          def render_rev(components: List[Component], data: Report.Data): XML.Body = {
+            val hg_info = data.component_logs.map(_._1) ++ data.component_diffs.map(_._1)
+            val s = components.mkString(", ")
 
-          def render_rev(components: List[Component], data: Report.Data): XML.Body = {
-            val relevant = non_local(components)
-            val hg_info = data.component_logs.map(_._1) ++ data.component_diffs.map(_._1)
-            val s = relevant.mkString(", ")
-
-            if (!relevant.map(_.name).exists(hg_info.toSet)) text(s)
+            if (!components.map(_.name).exists(hg_info.toSet)) text(s)
             else List(page_link(Page.DIFF, s, Markup.Name(build.name)))
           }
 
           build match {
             case task: Task =>
               par(text("Task from " + Build_Log.print_date(task.submit_date) + ". ")) ::
-              par(text(non_local(task.components).mkString(", "))) ::
+              par(text(task.components.mkString(", "))) ::
               render_cancel(task.uuid)
 
             case job: Job =>