# HG changeset patch # User wenzelm # Date 1605194851 -3600 # Node ID 76550282267f307d04cf70d1b135892b3289ed1d # Parent d9f2be66ebad457d9fbf43a4ccf4da39c50d6091 more interrupts, notably for running latex; diff -r d9f2be66ebad -r 76550282267f src/Pure/Admin/build_doc.scala --- a/src/Pure/Admin/build_doc.scala Thu Nov 12 16:07:25 2020 +0100 +++ b/src/Pure/Admin/build_doc.scala Thu Nov 12 16:27:31 2020 +0100 @@ -50,7 +50,6 @@ val errs = Par_List.map((doc_session: (String, String)) => try { - progress.expose_interrupt() Present.build_documents(doc_session._2, deps, store, progress = progress) None } diff -r d9f2be66ebad -r 76550282267f src/Pure/System/progress.scala --- a/src/Pure/System/progress.scala Thu Nov 12 16:07:25 2020 +0100 +++ b/src/Pure/System/progress.scala Thu Nov 12 16:27:31 2020 +0100 @@ -54,12 +54,16 @@ env: Map[String, String] = Isabelle_System.settings(), redirect: Boolean = false, echo: Boolean = false, + watchdog: Time = Time.zero, strict: Boolean = true): Process_Result = { - Isabelle_System.bash(script, cwd = cwd, env = env, redirect = redirect, - progress_stdout = echo_if(echo, _), - progress_stderr = echo_if(echo, _), - strict = strict) + val result = + Isabelle_System.bash(script, 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)), + strict = strict) + if (strict && stopped) throw Exn.Interrupt() else result } } diff -r d9f2be66ebad -r 76550282267f src/Pure/Thy/present.scala --- a/src/Pure/Thy/present.scala Thu Nov 12 16:07:25 2020 +0100 +++ b/src/Pure/Thy/present.scala Thu Nov 12 16:27:31 2020 +0100 @@ -278,7 +278,8 @@ "isabelle latex -o " + Bash.string(fmt) + " " + Bash.string(root + "." + ext) def bash(items: String*): Process_Result = - progress.bash(items.mkString(" && "), cwd = doc_dir.file, echo = verbose_latex) + progress.bash(items.mkString(" && "), cwd = doc_dir.file, + echo = verbose_latex, watchdog = Time.seconds(0.5)) // prepare document