1.1 --- a/src/HOL/Tools/ATP/atp_systems.ML Wed Oct 31 11:23:21 2012 +0100
1.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML Wed Oct 31 11:23:21 2012 +0100
1.3 @@ -581,13 +581,17 @@
1.4 val remote_systems = Synchronized.var "atp_remote_systems" ([] : string list)
1.5
1.6 fun get_remote_systems () =
1.7 - case Isabelle_System.bash_output
1.8 - "\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of
1.9 - (output, 0) => split_lines output
1.10 - | (output, _) =>
1.11 - error (case extract_known_failure known_perl_failures output of
1.12 - SOME failure => string_for_failure failure
1.13 - | NONE => trim_line output ^ ".")
1.14 + TimeLimit.timeLimit (seconds 10.0)
1.15 + (fn () =>
1.16 + case Isabelle_System.bash_output
1.17 + "\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of
1.18 + (output, 0) => split_lines output
1.19 + | (output, _) =>
1.20 + (warning (case extract_known_failure known_perl_failures output of
1.21 + SOME failure => string_for_failure failure
1.22 + | NONE => trim_line output ^ "."); [])) ()
1.23 + handle TimeLimit.TimeOut =>
1.24 + (warning "Cannot retrieve system list from SystemOnTPTP."; [])
1.25
1.26 fun find_remote_system name [] systems =
1.27 find_first (String.isPrefix (name ^ "---")) systems