src/Pure/Tools/build.scala
changeset 62569 5db10482f4cf
parent 62508 d0b68218ea55
child 62572 acd17a6ce17d
     1.1 --- a/src/Pure/Tools/build.scala	Wed Mar 09 14:24:16 2016 +0100
     1.2 +++ b/src/Pure/Tools/build.scala	Wed Mar 09 14:54:51 2016 +0100
     1.3 @@ -624,13 +624,11 @@
     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: Option[Time] = None
     1.8 +    @volatile private var was_timeout = false
     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(t0 + timeout) { terminate; was_timeout = Some(Time.now() - t0) })
    1.15 +      if (info.timeout > Time.zero)
    1.16 +        Some(Event_Timer.request(Time.now() + info.timeout) { terminate; was_timeout = true })
    1.17        else None
    1.18      }
    1.19  
    1.20 @@ -646,10 +644,8 @@
    1.21        timeout_request.foreach(_.cancel)
    1.22  
    1.23        if (res.interrupted) {
    1.24 -        was_timeout match {
    1.25 -          case Some(t) => res.error(Output.error_text("Timeout")).set_timeout(t)
    1.26 -          case None => res.error(Output.error_text("Interrupt"))
    1.27 -        }
    1.28 +        if (was_timeout) res.error(Output.error_text("Timeout")).was_timeout
    1.29 +        else res.error(Output.error_text("Interrupt"))
    1.30        }
    1.31        else res
    1.32      }