# HG changeset patch
# User wenzelm
# Date 1605193645 -3600
# Node ID d9f2be66ebad457d9fbf43a4ccf4da39c50d6091
# Parent  e8d7dc1c229c72302a76ac0c7fe23005b22a4f0e
support for watchdog thread;

diff -r e8d7dc1c229c -r d9f2be66ebad src/Pure/System/bash.scala
--- a/src/Pure/System/bash.scala	Thu Nov 12 12:34:36 2020 +0100
+++ b/src/Pure/System/bash.scala	Thu Nov 12 16:07:25 2020 +0100
@@ -45,6 +45,8 @@
 
   /* process and result */
 
+  type Watchdog = (Time, Process => Boolean)
+
   def process(script: String,
       cwd: JFile = null,
       env: Map[String, String] = Isabelle_System.settings(),
@@ -168,6 +170,7 @@
     def result(
       progress_stdout: String => Unit = (_: String) => (),
       progress_stderr: String => Unit = (_: String) => (),
+      watchdog: Option[Watchdog] = None,
       strict: Boolean = true): Process_Result =
     {
       stdin.close
@@ -177,9 +180,23 @@
       val err_lines =
         Future.thread("bash_stderr") { File.read_lines(stderr, progress_stderr) }
 
+      val watchdog_thread =
+        for ((time, check) <- watchdog)
+        yield {
+          Future.thread("bash_watchdog") {
+            while (proc.isAlive) {
+              time.sleep
+              if (check(this)) interrupt()
+            }
+          }
+        }
+
       val rc =
         try { join }
         catch { case Exn.Interrupt() => terminate(); Exn.Interrupt.return_code }
+
+      watchdog_thread.foreach(_.cancel)
+
       if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
 
       Process_Result(rc, out_lines.join, err_lines.join, false, get_timing)
diff -r e8d7dc1c229c -r d9f2be66ebad src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Thu Nov 12 12:34:36 2020 +0100
+++ b/src/Pure/System/isabelle_system.scala	Thu Nov 12 16:07:25 2020 +0100
@@ -347,11 +347,13 @@
     redirect: Boolean = false,
     progress_stdout: String => Unit = (_: String) => (),
     progress_stderr: String => Unit = (_: String) => (),
+    watchdog: Option[Bash.Watchdog] = None,
     strict: Boolean = true,
     cleanup: () => Unit = () => ()): Process_Result =
   {
     Bash.process(script, cwd = cwd, env = env, redirect = redirect, cleanup = cleanup).
-      result(progress_stdout, progress_stderr, strict)
+      result(progress_stdout = progress_stdout, progress_stderr = progress_stderr,
+        watchdog = watchdog, strict = strict)
   }
 
   def jconsole(): Process_Result =