# HG changeset patch
# User blanchet
# Date 1283765286 -7200
# Node ID f09b378cb2522086f006e6e8ca34e9e9efd1c05f
# Parent  fd179beb8cb395687bdbe3b99cafeb4d8a3d6ec0
make remote ATP invocation work for those people who need to go through a proxy;
thanks go to Mathieu G. for that fix

diff -r fd179beb8cb3 -r f09b378cb252 doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Sun Sep 05 21:39:30 2010 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Mon Sep 06 11:28:06 2010 +0200
@@ -159,7 +159,15 @@
 \S\ref{first-steps}.
 
 Remote ATP invocation via the SystemOnTPTP web service requires Perl with the
-World Wide Web Library (\texttt{libwww-perl}) installed.
+World Wide Web Library (\texttt{libwww-perl}) installed. If you must use a proxy
+server to access the Internet, set the \texttt{http\_proxy} environment variable
+to the proxy before launching Isabelle. Here are a few examples:
+
+\prew
+\texttt{export http\_proxy=http://proxy.example.org} \\
+\texttt{export http\_proxy=http://proxy.example.org:8080} \\
+\texttt{export http\_proxy=http://joeblow:pAsSwRd@proxy.example.org}
+\postw
 
 \section{First Steps}
 \label{first-steps}
diff -r fd179beb8cb3 -r f09b378cb252 src/HOL/Tools/ATP/scripts/remote_atp
--- a/src/HOL/Tools/ATP/scripts/remote_atp	Sun Sep 05 21:39:30 2010 +0200
+++ b/src/HOL/Tools/ATP/scripts/remote_atp	Mon Sep 06 11:28:06 2010 +0200
@@ -86,6 +86,7 @@
 
 # Query Server
 my $Agent = LWP::UserAgent->new;
+$Agent->env_proxy;
 if (exists($Options{'t'})) {
   # give server more time to respond
   $Agent->timeout($Options{'t'} + 10);