# HG changeset patch
# User wenzelm
# Date 1717271390 -7200
# Node ID 06036a16779f5f7d9f975157bd806e17c908cd0f
# Parent  cce5670be9f92d8c0e4db982b7cd645057ff1cc4
clarified signature: more explicit types;

diff -r cce5670be9f9 -r 06036a16779f src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Sat Jun 01 16:26:35 2024 +0200
+++ b/src/Pure/General/ssh.scala	Sat Jun 01 21:49:50 2024 +0200
@@ -567,7 +567,7 @@
         input: String = "",
         progress_stdout: String => Unit = (_: String) => (),
         progress_stderr: String => Unit = (_: String) => (),
-        watchdog: Option[Bash.Watchdog] = None,
+        watchdog: Bash.Watchdog = Bash.Watchdog.none,
         redirect: Boolean = false,
         settings: Boolean = true,
         strict: Boolean = true,
diff -r cce5670be9f9 -r 06036a16779f src/Pure/System/bash.scala
--- a/src/Pure/System/bash.scala	Sat Jun 01 16:26:35 2024 +0200
+++ b/src/Pure/System/bash.scala	Sat Jun 01 21:49:50 2024 +0200
@@ -74,7 +74,17 @@
     ssh.make_command(args_host = true, args = ssh.bash_path(exe))
   }
 
-  type Watchdog = (Time, Process => Boolean)
+  object Watchdog {
+    val none: Watchdog = new Watchdog(Time.zero, _ => false) {
+      override def toString: String = "Bash.Watchdog.none"
+    }
+    def apply(time: Time, check: Process => Boolean = _ => true): Watchdog =
+      if (time.is_zero) none else new Watchdog(time, check)
+  }
+  class Watchdog private(val time: Time, val check: Process => Boolean) {
+    override def toString: String = "Bash.Watchdog(" + time + ")"
+    def defined: Boolean = !time.is_zero
+  }
 
   def process(script: String,
       description: String = "",
@@ -248,7 +258,7 @@
       input: String = "",
       progress_stdout: String => Unit = (_: String) => (),
       progress_stderr: String => Unit = (_: String) => (),
-      watchdog: Option[Watchdog] = None,
+      watchdog: Watchdog = Watchdog.none,
       strict: Boolean = true
     ): Process_Result = {
       val in =
@@ -260,15 +270,16 @@
         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()
-            }
-          }
+        if (watchdog.defined) {
+          Some(
+            Future.thread("bash_watchdog") {
+              while (proc.isAlive) {
+                watchdog.time.sleep()
+                if (watchdog.check(this)) interrupt()
+              }
+            })
         }
+        else None
 
       val rc =
         try { join() }
@@ -377,8 +388,9 @@
 
               Isabelle_Thread.fork(name = "bash_process") {
                 @volatile var is_timeout = false
-                val watchdog: Option[Watchdog] =
-                  if (timeout.is_zero) None else Some((timeout, _ => { is_timeout = true; true }))
+                val watchdog =
+                  if (timeout.is_zero) Watchdog.none
+                  else Watchdog(timeout, _ => { is_timeout = true; true })
 
                 Exn.capture { process.result(input = input, watchdog = watchdog, strict = false) }
                 match {
diff -r cce5670be9f9 -r 06036a16779f src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Sat Jun 01 16:26:35 2024 +0200
+++ b/src/Pure/System/isabelle_system.scala	Sat Jun 01 21:49:50 2024 +0200
@@ -417,7 +417,7 @@
     input: String = "",
     progress_stdout: String => Unit = (_: String) => (),
     progress_stderr: String => Unit = (_: String) => (),
-    watchdog: Option[Bash.Watchdog] = None,
+    watchdog: Bash.Watchdog = Bash.Watchdog.none,
     strict: Boolean = true,
     cleanup: () => Unit = () => ()
   ): Process_Result = {
diff -r cce5670be9f9 -r 06036a16779f src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Sat Jun 01 16:26:35 2024 +0200
+++ b/src/Pure/System/progress.scala	Sat Jun 01 21:49:50 2024 +0200
@@ -105,7 +105,7 @@
       Isabelle_System.bash(script, ssh = ssh, cwd = cwd, env = env, redirect = redirect,
         progress_stdout = echo_if(echo, _),
         progress_stderr = echo_if(echo, _),
-        watchdog = if (watchdog.is_zero) None else Some((watchdog, _ => stopped)),
+        watchdog = Bash.Watchdog(watchdog, _ => stopped),
         strict = strict)
     if (strict && stopped) throw Exn.Interrupt() else result
   }