src/HOL/Tools/ATP/atp_systems.ML
changeset 51002 25e333d2eccd
parent 50999 9f655a6bffd8
child 51005 42209bfa1548
     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