--- a/etc/options Sun May 16 13:06:13 2021 +0200
+++ b/etc/options Sun May 16 13:14:16 2021 +0200
@@ -113,6 +113,9 @@
option timeout : real = 0
-- "timeout for session build job (seconds > 0)"
+option timeout_build : bool = true
+ -- "observe timeout for session build"
+
option process_output_limit : int = 100
-- "build process output limit (in million characters, 0 = unlimited)"
--- a/src/HOL/Tools/Mirabelle/mirabelle.scala Sun May 16 13:06:13 2021 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle.scala Sun May 16 13:14:16 2021 +0200
@@ -102,7 +102,7 @@
if (build_results0.ok) {
val build_options =
- options + "parallel_presentation=false" +
+ options + "timeout_build=false" + "parallel_presentation=false" +
("mirabelle_actions=" + actions.mkString(";")) +
("mirabelle_theories=" + theories.mkString(","))
--- a/src/Pure/Thy/sessions.scala Sun May 16 13:06:13 2021 +0200
+++ b/src/Pure/Thy/sessions.scala Sun May 16 13:14:16 2021 +0200
@@ -502,7 +502,9 @@
def dirs: List[Path] = dir :: directories
- def timeout_ignored: Boolean = Time.seconds(options.real("timeout")) < Time.ms(1)
+ def timeout_ignored: Boolean =
+ !options.bool("timeout_build") || Time.seconds(options.real("timeout")) < Time.ms(1)
+
def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale"))
def document_enabled: Boolean =