# HG changeset patch
# User wenzelm
# Date 1607610461 -3600
# Node ID 90e28f005be98e1cc2251ed33c541c48befe610f
# Parent  7b10b40b1273d6d226d406b50faa25040acd7349
tuned messages;

diff -r 7b10b40b1273 -r 90e28f005be9 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Thu Dec 10 15:21:55 2020 +0100
+++ b/src/Pure/Tools/build_job.scala	Thu Dec 10 15:27:41 2020 +0100
@@ -116,7 +116,7 @@
           val print_theories =
             if (theories.isEmpty) used_theories else used_theories.filter(theories.toSet)
           for (thy <- print_theories) {
-            val thy_heading = "Theory " + quote(thy) + ":"
+            val thy_heading = "\nTheory " + quote(thy) + ":"
             read_theory(db_context, resources, session_name, thy, unicode_symbols = unicode_symbols)
             match {
               case None => progress.echo(thy_heading + " MISSING")
@@ -137,7 +137,7 @@
 
           if (errors.nonEmpty) {
             val msg = Symbol.output(unicode_symbols, cat_lines(errors))
-            progress.echo("\nErrors:\n" + Output.error_message_text(msg))
+            progress.echo("\nBuild errors:\n" + Output.error_message_text(msg))
           }
           if (rc != 0) progress.echo("\n" + Process_Result.print_return_code(rc))
       }