1.1 --- a/src/Pure/System/build.scala	Sat Jul 28 19:48:19 2012 +0200
     1.2 +++ b/src/Pure/System/build.scala	Sat Jul 28 19:49:09 2012 +0200
     1.3 @@ -270,6 +270,7 @@
     1.4  
     1.5    sealed case class Deps(deps: Map[String, Node])
     1.6    {
     1.7 +    def is_empty: Boolean = deps.isEmpty
     1.8      def sources(name: String): List[SHA1.Digest] = deps(name).sources.map(_._2)
     1.9    }
    1.10  
    1.11 @@ -283,7 +284,12 @@
    1.12              }
    1.13            val thy_info = new Thy_Info(new Thy_Load(preloaded))
    1.14  
    1.15 -          if (verbose) echo("Checking " + name + " ...")
    1.16 +          if (verbose) {
    1.17 +            val groups =
    1.18 +              if (info.groups.isEmpty) ""
    1.19 +              else info.groups.mkString(" (", " ", ")")
    1.20 +            echo("Checking " + name + groups + " ...")
    1.21 +          }
    1.22  
    1.23            val thy_deps =
    1.24              thy_info.dependencies(
    1.25 @@ -539,7 +545,13 @@
    1.26          }
    1.27      }
    1.28  
    1.29 -    val results = loop(queue, Map.empty, Map.empty)
    1.30 +    val results =
    1.31 +      if (deps.is_empty) {
    1.32 +        echo("### Nothing to build")
    1.33 +        Map.empty
    1.34 +      }
    1.35 +      else loop(queue, Map.empty, Map.empty)
    1.36 +
    1.37      val rc = (0 /: results)({ case (rc1, (_, (_, rc2))) => rc1 max rc2 })
    1.38      if (rc != 0 && (verbose || !no_build)) {
    1.39        val unfinished =