# HG changeset patch
# User immler@in.tum.de
# Date 1237040144 -3600
# Node ID 0ac3db5a59a8ad820435ffe570a995ed8b0e8ad3
# Parent  ea4dabfea029dacf8a3f4ac4b6a71bb617cef592
removed connection check;
adapted times

diff -r ea4dabfea029 -r 0ac3db5a59a8 contrib/SystemOnTPTP/remote
--- a/contrib/SystemOnTPTP/remote	Sat Mar 14 12:51:13 2009 +0100
+++ b/contrib/SystemOnTPTP/remote	Sat Mar 14 15:15:44 2009 +0100
@@ -21,16 +21,6 @@
     "ProblemSource" => "UPLOAD",
     );
 
-# check connection
-my $TestAgent = LWP::UserAgent->new;
-$TestAgent->timeout(5);
-my $TestRequest = GET($SystemOnTPTPFormReplyURL);
-my $TestResponse = $TestAgent->request($TestRequest);
-if(! $TestResponse->is_success) {
-  print "HTTP-Error: " . $TestResponse->message . "\n";
-  exit(-1);
-}
-
 #----Get format and transform options if specified
 my %Options;
 getopts("hws:t:c:",\%Options);
@@ -85,7 +75,7 @@
 my $Agent = LWP::UserAgent->new;
 if (exists($Options{'t'})) {
   # give server more time to respond
-  $Agent->timeout($Options{'t'} * 2 + 10);
+  $Agent->timeout($Options{'t'} + 10);
 }
 my $Request = POST($SystemOnTPTPFormReplyURL,
 	Content_Type => 'form-data',Content => \%URLParameters);
diff -r ea4dabfea029 -r 0ac3db5a59a8 src/HOL/Tools/atp_wrapper.ML
--- a/src/HOL/Tools/atp_wrapper.ML	Sat Mar 14 12:51:13 2009 +0100
+++ b/src/HOL/Tools/atp_wrapper.ML	Sat Mar 14 15:15:44 2009 +0100
@@ -165,7 +165,7 @@
 
 fun remote_prover_opts max_new theory_const args timeout =
   tptp_prover_opts max_new theory_const
-  (Path.explode "$ISABELLE_HOME/contrib/SystemOnTPTP/remote", args ^ " -t " ^ string_of_int timeout)
+  (Path.explode "$ISABELLE_HOME/contrib/SystemOnTPTP/remote", args ^ " -t " ^ string_of_int (timeout - 10))
   timeout;
 
 val remote_prover = remote_prover_opts 60 false;