384 val process_result = job.join |
384 val process_result = job.join |
385 process_result.err_lines.foreach(progress.echo(_)) |
385 process_result.err_lines.foreach(progress.echo(_)) |
386 if (process_result.ok) |
386 if (process_result.ok) |
387 progress.echo("Finished " + name + " (" + process_result.timing.message_resources + ")") |
387 progress.echo("Finished " + name + " (" + process_result.timing.message_resources + ")") |
388 |
388 |
|
389 val log_lines = process_result.out_lines.filterNot(_.startsWith("\f")) |
389 val process_result_tail = |
390 val process_result_tail = |
390 { |
391 { |
391 val lines = process_result.out_lines.filterNot(_.startsWith("\f")) |
|
392 val tail = job.info.options.int("process_output_tail") |
392 val tail = job.info.options.int("process_output_tail") |
393 val lines1 = if (tail == 0) lines else lines.drop(lines.length - tail max 0) |
|
394 process_result.copy( |
393 process_result.copy( |
395 out_lines = |
394 out_lines = |
396 "(see also " + (store.output_dir + store.log(name)).file.toString + ")" :: |
395 "(see also " + (store.output_dir + store.log(name)).file.toString + ")" :: |
397 lines1) |
396 (if (tail == 0) log_lines else log_lines.drop(log_lines.length - tail max 0))) |
398 } |
397 } |
399 |
398 |
400 val heap_stamp = |
399 val heap_stamp = |
401 if (process_result.ok) { |
400 if (process_result.ok) { |
402 (store.output_dir + store.log(name)).file.delete |
401 (store.output_dir + store.log(name)).file.delete |
403 val heap_stamp = |
402 val heap_stamp = |
404 for (path <- job.output_path if path.is_file) |
403 for (path <- job.output_path if path.is_file) |
405 yield Sessions.write_heap_digest(path) |
404 yield Sessions.write_heap_digest(path) |
406 |
405 |
407 File.write_gzip(store.output_dir + store.log_gz(name), |
406 File.write_gzip(store.output_dir + store.log_gz(name), terminate_lines(log_lines)) |
408 terminate_lines(process_result.out_lines)) |
|
409 |
407 |
410 heap_stamp |
408 heap_stamp |
411 } |
409 } |
412 else { |
410 else { |
413 (store.output_dir + Path.basic(name)).file.delete |
411 (store.output_dir + Path.basic(name)).file.delete |
414 (store.output_dir + store.log_gz(name)).file.delete |
412 (store.output_dir + store.log_gz(name)).file.delete |
415 |
413 |
416 File.write(store.output_dir + store.log(name), |
414 File.write(store.output_dir + store.log(name), terminate_lines(log_lines)) |
417 terminate_lines(process_result.out_lines)) |
|
418 progress.echo(name + " FAILED") |
415 progress.echo(name + " FAILED") |
419 if (!process_result.interrupted) progress.echo(process_result_tail.out) |
416 if (!process_result.interrupted) progress.echo(process_result_tail.out) |
420 |
417 |
421 None |
418 None |
422 } |
419 } |