# HG changeset patch
# User wenzelm
# Date 1607605983 -3600
# Node ID a261946dafa3d500e7a303ec6add528c9a51f11d
# Parent  a7fa680d82774eae30750bea7ee7a628b0817574
tuned messages;

diff -r a7fa680d8277 -r a261946dafa3 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Wed Dec 09 23:30:12 2020 +0100
+++ b/src/Pure/Tools/build_job.scala	Thu Dec 10 14:13:03 2020 +0100
@@ -102,17 +102,20 @@
           val print_theories =
             if (theories.isEmpty) used_theories else used_theories.filter(theories.toSet)
           for (thy <- print_theories) {
-            val thy_heading = "\nTheory " + quote(thy)
+            val thy_heading = "Theory " + quote(thy) + ":"
             read_theory(db_context, resources, session_name, thy) match {
-              case None => progress.echo(thy_heading + ": MISSING")
+              case None => progress.echo(thy_heading + " MISSING")
               case Some(command) =>
-                progress.echo(thy_heading)
                 val snapshot = Document.State.init.command_snippet(command)
                 val rendering = new Rendering(snapshot, options, session)
-                for (Text.Info(_, t) <- rendering.text_messages(Text.Range.full)) {
-                  progress.echo(
-                    Protocol.message_text(List(t), margin = margin, breakgain = breakgain,
-                      metric = metric))
+                val messages = rendering.text_messages(Text.Range.full)
+                if (messages.nonEmpty) {
+                  progress.echo(thy_heading)
+                  for (Text.Info(_, t) <- messages) {
+                    progress.echo(
+                      Protocol.message_text(List(t), margin = margin, breakgain = breakgain,
+                        metric = metric))
+                  }
                 }
             }
           }