clarified messages: after writing all files (see also 27f90319a499 and 57c85c83c11b);
--- a/src/Pure/Tools/build.scala Mon Sep 11 17:55:42 2017 +0200
+++ b/src/Pure/Tools/build.scala Fri Sep 15 17:50:52 2017 +0200
@@ -455,9 +455,6 @@
//{{{ finish job
val process_result = job.join
- process_result.err_lines.foreach(progress.echo(_))
- if (process_result.ok)
- progress.echo("Finished " + name + " (" + process_result.timing.message_resources + ")")
val log_lines = process_result.out_lines.filterNot(_.startsWith("\f"))
val process_result_tail =
@@ -469,6 +466,8 @@
(if (tail == 0) log_lines else log_lines.drop(log_lines.length - tail max 0)))
}
+
+ // write log file
val heap_stamp =
if (process_result.ok) {
(store.output_dir + store.log(name)).file.delete
@@ -485,8 +484,6 @@
(store.output_dir + store.log_gz(name)).file.delete
File.write(store.output_dir + store.log(name), terminate_lines(log_lines))
- progress.echo(name + " FAILED")
- if (!process_result.interrupted) progress.echo(process_result_tail.out)
None
}
@@ -506,6 +503,16 @@
Session_Info(sources_stamp(name), input_heaps, heap_stamp, process_result.rc)))
}
+ // messages
+ process_result.err_lines.foreach(progress.echo(_))
+
+ if (process_result.ok)
+ progress.echo("Finished " + name + " (" + process_result.timing.message_resources + ")")
+ else {
+ progress.echo(name + " FAILED")
+ if (!process_result.interrupted) progress.echo(process_result_tail.out)
+ }
+
loop(pending - name, running - name,
results + (name -> Result(false, heap_stamp, Some(process_result_tail), job.info)))
//}}}