# HG changeset patch
# User wenzelm
# Date 1457538794 -3600
# Node ID acd17a6ce17d79434fd3a5f1ae933e8eb5b99d04
# Parent  2fd90993a92810586325a576e7621954e89b2c91
tuned;

diff -r 2fd90993a928 -r acd17a6ce17d src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Mar 09 16:42:30 2016 +0100
+++ b/src/Pure/Tools/build.scala	Wed Mar 09 16:53:14 2016 +0100
@@ -605,7 +605,7 @@
       exit "$RC"
       """
 
-    private val result =
+    private val future_result =
       Future.thread("build") {
         Isabelle_System.bash(script, info.dir.file, env,
           progress_stdout = (line: String) =>
@@ -621,8 +621,8 @@
           strict = false)
       }
 
-    def terminate: Unit = result.cancel
-    def is_finished: Boolean = result.is_finished
+    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] =
@@ -634,20 +634,20 @@
 
     def join: Process_Result =
     {
-      val res = result.join
+      val result = future_result.join
 
-      if (res.ok && !is_pure(name))
+      if (result.ok && !is_pure(name))
         Present.finish(progress, browser_info, graph_file, info, name)
 
       graph_file.delete
       args_file.delete
       timeout_request.foreach(_.cancel)
 
-      if (res.interrupted) {
-        if (was_timeout) res.error(Output.error_text("Timeout")).was_timeout
-        else res.error(Output.error_text("Interrupt"))
+      if (result.interrupted) {
+        if (was_timeout) result.error(Output.error_text("Timeout")).was_timeout
+        else result.error(Output.error_text("Interrupt"))
       }
-      else res
+      else result
     }
   }