6 */ |
6 */ |
7 |
7 |
8 package isabelle |
8 package isabelle |
9 |
9 |
10 |
10 |
11 import java.util.{Timer, TimerTask} |
|
12 import java.io.{BufferedInputStream, FileInputStream, |
11 import java.io.{BufferedInputStream, FileInputStream, |
13 BufferedReader, InputStreamReader, IOException} |
12 BufferedReader, InputStreamReader, IOException} |
14 import java.util.zip.GZIPInputStream |
13 import java.util.zip.GZIPInputStream |
15 |
14 |
16 import scala.collection.SortedSet |
15 import scala.collection.SortedSet |
588 } |
587 } |
589 |
588 |
590 def terminate: Unit = thread.interrupt |
589 def terminate: Unit = thread.interrupt |
591 def is_finished: Boolean = result.is_finished |
590 def is_finished: Boolean = result.is_finished |
592 |
591 |
593 @volatile private var timeout = false |
592 @volatile private var was_timeout = false |
594 private val time = info.options.seconds("timeout") |
593 private val timeout_request: Option[Event_Timer.Request] = |
595 private val timer: Option[Timer] = |
594 { |
596 if (time.seconds > 0.0) { |
595 val timeout = info.options.seconds("timeout") |
597 val t = new Timer("build", true) |
596 if (timeout > Time.zero) |
598 t.schedule(new TimerTask { def run = { terminate; timeout = true } }, time.ms) |
597 Some(Event_Timer.request(Time.now() + timeout) { terminate; was_timeout = true }) |
599 Some(t) |
|
600 } |
|
601 else None |
598 else None |
|
599 } |
602 |
600 |
603 def join: Isabelle_System.Bash_Result = |
601 def join: Isabelle_System.Bash_Result = |
604 { |
602 { |
605 val res = result.join |
603 val res = result.join |
606 |
604 |
607 args_file.delete |
605 args_file.delete |
608 timer.map(_.cancel()) |
606 timeout_request.foreach(_.cancel) |
609 |
607 |
610 if (res.rc == Exn.Interrupt.return_code) { |
608 if (res.rc == Exn.Interrupt.return_code) { |
611 if (timeout) res.add_err("*** Timeout").set_rc(1) |
609 if (was_timeout) res.add_err("*** Timeout").set_rc(1) |
612 else res.add_err("*** Interrupt") |
610 else res.add_err("*** Interrupt") |
613 } |
611 } |
614 else res |
612 else res |
615 } |
613 } |
616 } |
614 } |