clarified: adapted to ML version;
authorwenzelm
Mon, 30 Oct 2017 18:39:30 +0100
changeset 66943 351aaaa9bacd
parent 66942 91a21a5631ae
child 66944 05df740cb54b
clarified: adapted to ML version;
src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Mon Oct 30 17:06:02 2017 +0100
+++ b/src/Pure/Tools/build.scala	Mon Oct 30 18:39:30 2017 +0100
@@ -298,11 +298,10 @@
     def terminate: Unit = future_result.cancel
     def is_finished: Boolean = future_result.is_finished
 
-    @volatile private var was_timeout = false
     private val timeout_request: Option[Event_Timer.Request] =
     {
       if (info.timeout > Time.zero)
-        Some(Event_Timer.request(Time.now() + info.timeout) { terminate; was_timeout = true })
+        Some(Event_Timer.request(Time.now() + info.timeout) { terminate })
       else None
     }
 
@@ -314,7 +313,12 @@
         Present.finish(progress, store.browser_info, graph_file, info, name)
 
       graph_file.delete
-      timeout_request.foreach(_.cancel)
+
+      val was_timeout =
+        timeout_request match {
+          case None => false
+          case Some(request) => !request.cancel
+        }
 
       if (result.interrupted) {
         if (was_timeout) result.error(Output.error_message_text("Timeout")).was_timeout