# HG changeset patch
# User blanchet
# Date 1351679001 -3600
# Node ID 25e333d2eccd095e083215b4437896ffd0a0adab
# Parent  90e7be285b497a7e5eac616e0b26e1c5a809e9b7
added a timeout around script that relies on the network

diff -r 90e7be285b49 -r 25e333d2eccd src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Wed Oct 31 11:23:21 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Wed Oct 31 11:23:21 2012 +0100
@@ -581,13 +581,17 @@
 val remote_systems = Synchronized.var "atp_remote_systems" ([] : string list)
 
 fun get_remote_systems () =
-  case Isabelle_System.bash_output
-           "\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of
-    (output, 0) => split_lines output
-  | (output, _) =>
-    error (case extract_known_failure known_perl_failures output of
-             SOME failure => string_for_failure failure
-           | NONE => trim_line output ^ ".")
+  TimeLimit.timeLimit (seconds 10.0)
+    (fn () =>
+        case Isabelle_System.bash_output
+            "\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of
+          (output, 0) => split_lines output
+        | (output, _) =>
+          (warning (case extract_known_failure known_perl_failures output of
+                      SOME failure => string_for_failure failure
+                    | NONE => trim_line output ^ "."); [])) ()
+  handle TimeLimit.TimeOut =>
+         (warning "Cannot retrieve system list from SystemOnTPTP."; [])
 
 fun find_remote_system name [] systems =
     find_first (String.isPrefix (name ^ "---")) systems