clarified: adapted to ML version;
authorwenzelm
Mon Oct 30 18:39:30 2017 +0100 (19 months ago)
changeset 66943351aaaa9bacd
parent 66942 91a21a5631ae
child 66944 05df740cb54b
clarified: adapted to ML version;
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/Tools/build.scala	Mon Oct 30 17:06:02 2017 +0100
     1.2 +++ b/src/Pure/Tools/build.scala	Mon Oct 30 18:39:30 2017 +0100
     1.3 @@ -298,11 +298,10 @@
     1.4      def terminate: Unit = future_result.cancel
     1.5      def is_finished: Boolean = future_result.is_finished
     1.6  
     1.7 -    @volatile private var was_timeout = false
     1.8      private val timeout_request: Option[Event_Timer.Request] =
     1.9      {
    1.10        if (info.timeout > Time.zero)
    1.11 -        Some(Event_Timer.request(Time.now() + info.timeout) { terminate; was_timeout = true })
    1.12 +        Some(Event_Timer.request(Time.now() + info.timeout) { terminate })
    1.13        else None
    1.14      }
    1.15  
    1.16 @@ -314,7 +313,12 @@
    1.17          Present.finish(progress, store.browser_info, graph_file, info, name)
    1.18  
    1.19        graph_file.delete
    1.20 -      timeout_request.foreach(_.cancel)
    1.21 +
    1.22 +      val was_timeout =
    1.23 +        timeout_request match {
    1.24 +          case None => false
    1.25 +          case Some(request) => !request.cancel
    1.26 +        }
    1.27  
    1.28        if (result.interrupted) {
    1.29          if (was_timeout) result.error(Output.error_message_text("Timeout")).was_timeout