src/Pure/Tools/build.scala
changeset 65278 b553d0edc440
parent 65253 85c0ac5c2589
child 65281 c70e7d24a16d
equal deleted inserted replaced
65277:e9f9f962828d 65278:b553d0edc440
   370 
   370 
   371     // optional cleanup
   371     // optional cleanup
   372     if (clean_build) {
   372     if (clean_build) {
   373       for (name <- full_tree.graph.all_succs(selected)) {
   373       for (name <- full_tree.graph.all_succs(selected)) {
   374         val files =
   374         val files =
   375           List(Path.basic(name), Sessions.log(name), Sessions.log_gz(name)).
   375           List(Path.basic(name), store.log(name), store.log_gz(name)).
   376             map(store.output_dir + _).filter(_.is_file)
   376             map(store.output_dir + _).filter(_.is_file)
   377         if (files.nonEmpty) progress.echo("Cleaning " + name + " ...")
   377         if (files.nonEmpty) progress.echo("Cleaning " + name + " ...")
   378         if (!files.forall(p => p.file.delete)) progress.echo(name + " FAILED to delete")
   378         if (!files.forall(p => p.file.delete)) progress.echo(name + " FAILED to delete")
   379       }
   379       }
   380     }
   380     }
   427               val lines = process_result.out_lines.filterNot(_.startsWith("\f"))
   427               val lines = process_result.out_lines.filterNot(_.startsWith("\f"))
   428               val tail = job.info.options.int("process_output_tail")
   428               val tail = job.info.options.int("process_output_tail")
   429               val lines1 = if (tail == 0) lines else lines.drop(lines.length - tail max 0)
   429               val lines1 = if (tail == 0) lines else lines.drop(lines.length - tail max 0)
   430               process_result.copy(
   430               process_result.copy(
   431                 out_lines =
   431                 out_lines =
   432                   "(see also " + (store.output_dir + Sessions.log(name)).file.toString + ")" ::
   432                   "(see also " + (store.output_dir + store.log(name)).file.toString + ")" ::
   433                   lines1)
   433                   lines1)
   434             }
   434             }
   435 
   435 
   436             val heap_stamp =
   436             val heap_stamp =
   437               if (process_result.ok) {
   437               if (process_result.ok) {
   438                 (store.output_dir + Sessions.log(name)).file.delete
   438                 (store.output_dir + store.log(name)).file.delete
   439                 val heap_stamp =
   439                 val heap_stamp =
   440                   for (path <- job.output_path if path.is_file)
   440                   for (path <- job.output_path if path.is_file)
   441                     yield Sessions.write_heap_digest(path)
   441                     yield Sessions.write_heap_digest(path)
   442 
   442 
   443                 File.write_gzip(store.output_dir + Sessions.log_gz(name),
   443                 File.write_gzip(store.output_dir + store.log_gz(name),
   444                   terminate_lines(
   444                   terminate_lines(
   445                     session_sources_stamp(name) ::
   445                     session_sources_stamp(name) ::
   446                     input_heaps.map(INPUT_HEAP + _) :::
   446                     input_heaps.map(INPUT_HEAP + _) :::
   447                     heap_stamp.toList.map(OUTPUT_HEAP + _) :::
   447                     heap_stamp.toList.map(OUTPUT_HEAP + _) :::
   448                     List(LOG_START) ::: process_result.out_lines))
   448                     List(LOG_START) ::: process_result.out_lines))
   449 
   449 
   450                 heap_stamp
   450                 heap_stamp
   451               }
   451               }
   452               else {
   452               else {
   453                 (store.output_dir + Path.basic(name)).file.delete
   453                 (store.output_dir + Path.basic(name)).file.delete
   454                 (store.output_dir + Sessions.log_gz(name)).file.delete
   454                 (store.output_dir + store.log_gz(name)).file.delete
   455 
   455 
   456                 File.write(store.output_dir + Sessions.log(name),
   456                 File.write(store.output_dir + store.log(name),
   457                   terminate_lines(process_result.out_lines))
   457                   terminate_lines(process_result.out_lines))
   458                 progress.echo(name + " FAILED")
   458                 progress.echo(name + " FAILED")
   459                 if (!process_result.interrupted) progress.echo(process_result_tail.out)
   459                 if (!process_result.interrupted) progress.echo(process_result_tail.out)
   460 
   460 
   461                 None
   461                 None