# HG changeset patch
# User wenzelm
# Date 1509385170 -3600
# Node ID 351aaaa9bacdcee775f1119c5645edb9bf423d3f
# Parent  91a21a5631ae1705c6401d0a2cdb47a32e046f51
clarified: adapted to ML version;

diff -r 91a21a5631ae -r 351aaaa9bacd 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