src/Pure/Tools/build.scala
changeset 56779 9823818588fb
parent 56668 56335a8e2e8b
child 56780 e76467fed375
equal deleted inserted replaced
56778:cb0929421ca6 56779:9823818588fb
     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   }