# HG changeset patch
# User wenzelm
# Date 1343497749 -7200
# Node ID ed975dbb16ca8686a609b88fb8cda69b8a5b4cfc
# Parent  c6bed330fc073ed6013db99c8ae94a4d375f8eb0
tuned messages;

diff -r c6bed330fc07 -r ed975dbb16ca src/Pure/System/build.scala
--- a/src/Pure/System/build.scala	Sat Jul 28 19:48:19 2012 +0200
+++ b/src/Pure/System/build.scala	Sat Jul 28 19:49:09 2012 +0200
@@ -270,6 +270,7 @@
 
   sealed case class Deps(deps: Map[String, Node])
   {
+    def is_empty: Boolean = deps.isEmpty
     def sources(name: String): List[SHA1.Digest] = deps(name).sources.map(_._2)
   }
 
@@ -283,7 +284,12 @@
             }
           val thy_info = new Thy_Info(new Thy_Load(preloaded))
 
-          if (verbose) echo("Checking " + name + " ...")
+          if (verbose) {
+            val groups =
+              if (info.groups.isEmpty) ""
+              else info.groups.mkString(" (", " ", ")")
+            echo("Checking " + name + groups + " ...")
+          }
 
           val thy_deps =
             thy_info.dependencies(
@@ -539,7 +545,13 @@
         }
     }
 
-    val results = loop(queue, Map.empty, Map.empty)
+    val results =
+      if (deps.is_empty) {
+        echo("### Nothing to build")
+        Map.empty
+      }
+      else loop(queue, Map.empty, Map.empty)
+
     val rc = (0 /: results)({ case (rc1, (_, (_, rc2))) => rc1 max rc2 })
     if (rc != 0 && (verbose || !no_build)) {
       val unfinished =