src/Pure/Tools/build.scala
changeset 66666 1a620647285c
parent 66595 fa10b0f589c3
child 66712 4c98c929a12a
     1.1 --- a/src/Pure/Tools/build.scala	Mon Sep 11 17:55:42 2017 +0200
     1.2 +++ b/src/Pure/Tools/build.scala	Fri Sep 15 17:50:52 2017 +0200
     1.3 @@ -455,9 +455,6 @@
     1.4              //{{{ finish job
     1.5  
     1.6              val process_result = job.join
     1.7 -            process_result.err_lines.foreach(progress.echo(_))
     1.8 -            if (process_result.ok)
     1.9 -              progress.echo("Finished " + name + " (" + process_result.timing.message_resources + ")")
    1.10  
    1.11              val log_lines = process_result.out_lines.filterNot(_.startsWith("\f"))
    1.12              val process_result_tail =
    1.13 @@ -469,6 +466,8 @@
    1.14                    (if (tail == 0) log_lines else log_lines.drop(log_lines.length - tail max 0)))
    1.15              }
    1.16  
    1.17 +
    1.18 +            // write log file
    1.19              val heap_stamp =
    1.20                if (process_result.ok) {
    1.21                  (store.output_dir + store.log(name)).file.delete
    1.22 @@ -485,8 +484,6 @@
    1.23                  (store.output_dir + store.log_gz(name)).file.delete
    1.24  
    1.25                  File.write(store.output_dir + store.log(name), terminate_lines(log_lines))
    1.26 -                progress.echo(name + " FAILED")
    1.27 -                if (!process_result.interrupted) progress.echo(process_result_tail.out)
    1.28  
    1.29                  None
    1.30                }
    1.31 @@ -506,6 +503,16 @@
    1.32                      Session_Info(sources_stamp(name), input_heaps, heap_stamp, process_result.rc)))
    1.33              }
    1.34  
    1.35 +            // messages
    1.36 +            process_result.err_lines.foreach(progress.echo(_))
    1.37 +
    1.38 +            if (process_result.ok)
    1.39 +              progress.echo("Finished " + name + " (" + process_result.timing.message_resources + ")")
    1.40 +            else {
    1.41 +              progress.echo(name + " FAILED")
    1.42 +              if (!process_result.interrupted) progress.echo(process_result_tail.out)
    1.43 +            }
    1.44 +
    1.45              loop(pending - name, running - name,
    1.46                results + (name -> Result(false, heap_stamp, Some(process_result_tail), job.info)))
    1.47              //}}}