added a timeout around script that relies on the network
authorblanchet
Wed, 31 Oct 2012 11:23:21 +0100
changeset 49987 25e333d2eccd
parent 49986 90e7be285b49
child 49988 ef811090e106
added a timeout around script that relies on the network
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