src/Pure/Tools/build.scala
changeset 62401 15a2533f1f0a
parent 62400 833af0d6d469
child 62402 bff56eae3ec5
     1.1 --- a/src/Pure/Tools/build.scala	Wed Feb 24 22:11:28 2016 +0100
     1.2 +++ b/src/Pure/Tools/build.scala	Wed Feb 24 22:40:19 2016 +0100
     1.3 @@ -619,12 +619,13 @@
     1.4      def terminate: Unit = result.cancel
     1.5      def is_finished: Boolean = result.is_finished
     1.6  
     1.7 -    @volatile private var was_timeout = false
     1.8 +    @volatile private var was_timeout: Option[Time] = None
     1.9      private val timeout_request: Option[Event_Timer.Request] =
    1.10      {
    1.11        val timeout = info.timeout
    1.12 +      val t0 = Time.now()
    1.13        if (timeout > Time.zero)
    1.14 -        Some(Event_Timer.request(Time.now() + timeout) { terminate; was_timeout = true })
    1.15 +        Some(Event_Timer.request(t0 + timeout) { terminate; was_timeout = Some(Time.now() - t0) })
    1.16        else None
    1.17      }
    1.18  
    1.19 @@ -639,9 +640,11 @@
    1.20        args_file.delete
    1.21        timeout_request.foreach(_.cancel)
    1.22  
    1.23 -      if (res.rc == Exn.Interrupt.return_code) {
    1.24 -        if (was_timeout) res.error(Output.error_text("Timeout"), 1)
    1.25 -        else res.error(Output.error_text("Interrupt"))
    1.26 +      if (res.interrupted) {
    1.27 +        was_timeout match {
    1.28 +          case Some(t) => res.error(Output.error_text("Timeout"), 1).set_timeout(t)
    1.29 +          case None => res.error(Output.error_text("Interrupt"))
    1.30 +        }
    1.31        }
    1.32        else res
    1.33      }
    1.34 @@ -854,17 +857,17 @@
    1.35            case Some((name, (parent_heap, job))) =>
    1.36              //{{{ finish job
    1.37  
    1.38 -            val res = job.join
    1.39 -            progress.echo(res.err)
    1.40 +            val process_result = job.join
    1.41 +            progress.echo(process_result.err)
    1.42  
    1.43              val heap =
    1.44 -              if (res.ok) {
    1.45 +              if (process_result.ok) {
    1.46                  (output_dir + log(name)).file.delete
    1.47  
    1.48                  val sources = make_stamp(name)
    1.49                  val heap = heap_stamp(job.output_path)
    1.50                  File.write_gzip(output_dir + log_gz(name),
    1.51 -                  Library.terminate_lines(sources :: parent_heap :: heap :: res.out_lines))
    1.52 +                  Library.terminate_lines(sources :: parent_heap :: heap :: process_result.out_lines))
    1.53  
    1.54                  heap
    1.55                }
    1.56 @@ -872,11 +875,11 @@
    1.57                  (output_dir + Path.basic(name)).file.delete
    1.58                  (output_dir + log_gz(name)).file.delete
    1.59  
    1.60 -                File.write(output_dir + log(name), Library.terminate_lines(res.out_lines))
    1.61 +                File.write(output_dir + log(name), Library.terminate_lines(process_result.out_lines))
    1.62                  progress.echo(name + " FAILED")
    1.63 -                if (res.rc != Exn.Interrupt.return_code) {
    1.64 +                if (!process_result.interrupted) {
    1.65                    progress.echo("(see also " + (output_dir + log(name)).file.toString + ")")
    1.66 -                  val lines = res.out_lines.filterNot(_.startsWith("\f"))
    1.67 +                  val lines = process_result.out_lines.filterNot(_.startsWith("\f"))
    1.68                    val tail = lines.drop(lines.length - 20 max 0)
    1.69                    progress.echo("\n" + cat_lines(tail))
    1.70                  }
    1.71 @@ -884,7 +887,7 @@
    1.72                  no_heap
    1.73                }
    1.74              loop(pending - name, running - name,
    1.75 -              results + (name -> Result(false, heap, res.rc)))
    1.76 +              results + (name -> Result(false, heap, process_result.rc)))
    1.77              //}}}
    1.78            case None if running.size < (max_jobs max 1) =>
    1.79              //{{{ check/start next job