tuned -- prefer Isabelle/Scala operations;
authorwenzelm
Tue Apr 29 11:14:39 2014 +0200 (2014-04-29)
changeset 567799823818588fb
parent 56778 cb0929421ca6
child 56780 e76467fed375
tuned -- prefer Isabelle/Scala operations;
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/Tools/build.scala	Mon Apr 28 23:43:13 2014 +0200
     1.2 +++ b/src/Pure/Tools/build.scala	Tue Apr 29 11:14:39 2014 +0200
     1.3 @@ -8,7 +8,6 @@
     1.4  package isabelle
     1.5  
     1.6  
     1.7 -import java.util.{Timer, TimerTask}
     1.8  import java.io.{BufferedInputStream, FileInputStream,
     1.9    BufferedReader, InputStreamReader, IOException}
    1.10  import java.util.zip.GZIPInputStream
    1.11 @@ -590,25 +589,24 @@
    1.12      def terminate: Unit = thread.interrupt
    1.13      def is_finished: Boolean = result.is_finished
    1.14  
    1.15 -    @volatile private var timeout = false
    1.16 -    private val time = info.options.seconds("timeout")
    1.17 -    private val timer: Option[Timer] =
    1.18 -      if (time.seconds > 0.0) {
    1.19 -        val t = new Timer("build", true)
    1.20 -        t.schedule(new TimerTask { def run = { terminate; timeout = true } }, time.ms)
    1.21 -        Some(t)
    1.22 -      }
    1.23 +    @volatile private var was_timeout = false
    1.24 +    private val timeout_request: Option[Event_Timer.Request] =
    1.25 +    {
    1.26 +      val timeout = info.options.seconds("timeout")
    1.27 +      if (timeout > Time.zero)
    1.28 +        Some(Event_Timer.request(Time.now() + timeout) { terminate; was_timeout = true })
    1.29        else None
    1.30 +    }
    1.31  
    1.32      def join: Isabelle_System.Bash_Result =
    1.33      {
    1.34        val res = result.join
    1.35  
    1.36        args_file.delete
    1.37 -      timer.map(_.cancel())
    1.38 +      timeout_request.foreach(_.cancel)
    1.39  
    1.40        if (res.rc == Exn.Interrupt.return_code) {
    1.41 -        if (timeout) res.add_err("*** Timeout").set_rc(1)
    1.42 +        if (was_timeout) res.add_err("*** Timeout").set_rc(1)
    1.43          else res.add_err("*** Interrupt")
    1.44        }
    1.45        else res