src/Pure/Tools/build_job.scala
changeset 72868 90e28f005be9
parent 72867 7b10b40b1273
child 72869 015a61936c13
equal deleted inserted replaced
72867:7b10b40b1273 72868:90e28f005be9
   114           if (bad_theories.nonEmpty) error("Unknown theories " + commas_quote(bad_theories))
   114           if (bad_theories.nonEmpty) error("Unknown theories " + commas_quote(bad_theories))
   115 
   115 
   116           val print_theories =
   116           val print_theories =
   117             if (theories.isEmpty) used_theories else used_theories.filter(theories.toSet)
   117             if (theories.isEmpty) used_theories else used_theories.filter(theories.toSet)
   118           for (thy <- print_theories) {
   118           for (thy <- print_theories) {
   119             val thy_heading = "Theory " + quote(thy) + ":"
   119             val thy_heading = "\nTheory " + quote(thy) + ":"
   120             read_theory(db_context, resources, session_name, thy, unicode_symbols = unicode_symbols)
   120             read_theory(db_context, resources, session_name, thy, unicode_symbols = unicode_symbols)
   121             match {
   121             match {
   122               case None => progress.echo(thy_heading + " MISSING")
   122               case None => progress.echo(thy_heading + " MISSING")
   123               case Some(command) =>
   123               case Some(command) =>
   124                 val snapshot = Document.State.init.command_snippet(command)
   124                 val snapshot = Document.State.init.command_snippet(command)
   135             }
   135             }
   136           }
   136           }
   137 
   137 
   138           if (errors.nonEmpty) {
   138           if (errors.nonEmpty) {
   139             val msg = Symbol.output(unicode_symbols, cat_lines(errors))
   139             val msg = Symbol.output(unicode_symbols, cat_lines(errors))
   140             progress.echo("\nErrors:\n" + Output.error_message_text(msg))
   140             progress.echo("\nBuild errors:\n" + Output.error_message_text(msg))
   141           }
   141           }
   142           if (rc != 0) progress.echo("\n" + Process_Result.print_return_code(rc))
   142           if (rc != 0) progress.echo("\n" + Process_Result.print_return_code(rc))
   143       }
   143       }
   144     })
   144     })
   145   }
   145   }