tuned;
authorwenzelm
Wed Mar 09 16:53:14 2016 +0100 (2016-03-09)
changeset 62572acd17a6ce17d
parent 62571 2fd90993a928
child 62573 27f90319a499
tuned;
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/Tools/build.scala	Wed Mar 09 16:42:30 2016 +0100
     1.2 +++ b/src/Pure/Tools/build.scala	Wed Mar 09 16:53:14 2016 +0100
     1.3 @@ -605,7 +605,7 @@
     1.4        exit "$RC"
     1.5        """
     1.6  
     1.7 -    private val result =
     1.8 +    private val future_result =
     1.9        Future.thread("build") {
    1.10          Isabelle_System.bash(script, info.dir.file, env,
    1.11            progress_stdout = (line: String) =>
    1.12 @@ -621,8 +621,8 @@
    1.13            strict = false)
    1.14        }
    1.15  
    1.16 -    def terminate: Unit = result.cancel
    1.17 -    def is_finished: Boolean = result.is_finished
    1.18 +    def terminate: Unit = future_result.cancel
    1.19 +    def is_finished: Boolean = future_result.is_finished
    1.20  
    1.21      @volatile private var was_timeout = false
    1.22      private val timeout_request: Option[Event_Timer.Request] =
    1.23 @@ -634,20 +634,20 @@
    1.24  
    1.25      def join: Process_Result =
    1.26      {
    1.27 -      val res = result.join
    1.28 +      val result = future_result.join
    1.29  
    1.30 -      if (res.ok && !is_pure(name))
    1.31 +      if (result.ok && !is_pure(name))
    1.32          Present.finish(progress, browser_info, graph_file, info, name)
    1.33  
    1.34        graph_file.delete
    1.35        args_file.delete
    1.36        timeout_request.foreach(_.cancel)
    1.37  
    1.38 -      if (res.interrupted) {
    1.39 -        if (was_timeout) res.error(Output.error_text("Timeout")).was_timeout
    1.40 -        else res.error(Output.error_text("Interrupt"))
    1.41 +      if (result.interrupted) {
    1.42 +        if (was_timeout) result.error(Output.error_text("Timeout")).was_timeout
    1.43 +        else result.error(Output.error_text("Interrupt"))
    1.44        }
    1.45 -      else res
    1.46 +      else result
    1.47      }
    1.48    }
    1.49