# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1719330937 -7200
# Node ID fc26d6200560ce159c500205652f8e2e1d358f01
# Parent  d85ad13d8cf32fe081614388f5ca0494c7771675
clarified;

diff -r d85ad13d8cf3 -r fc26d6200560 src/Pure/Build/build_manager.scala
--- a/src/Pure/Build/build_manager.scala	Tue Jun 25 13:53:45 2024 +0200
+++ b/src/Pure/Build/build_manager.scala	Tue Jun 25 17:55:37 2024 +0200
@@ -26,6 +26,8 @@
 
   case class Component(name: String, rev: String = "") {
     override def toString: String = name + "/" + rev
+
+    def is_local: Boolean = rev.isEmpty
   }
 
   sealed trait Build_Config {
@@ -762,7 +764,7 @@
                   val target = context.task_dir + sync_dir.target
                   component.copy(rev = sync(sync_dir.hg, component.rev, target))
                 case None =>
-                  if (component.rev.isEmpty) component
+                  if (component.is_local) component
                   else error("Unknown component " + component)
               }
 
@@ -774,7 +776,7 @@
 
               for {
                 component <- Component("Isabelle", job.isabelle_rev) :: job.components
-                if component.rev.nonEmpty
+                if !component.is_local
               } context.progress.echo("Using " + component.toString)
 
               Some(context)
@@ -1088,7 +1090,7 @@
           def render_rev(isabelle_rev: String, components: List[Component]): XML.Body =
             for {
               component <- Component("Isabelle", isabelle_rev) :: components
-              if component.rev.nonEmpty
+              if !component.is_local
             } yield par(text(component.toString))
 
           build match {