# HG changeset patch
# User blanchet
# Date 1280389309 -7200
# Node ID 9069e1ad15272ada410182926c8892db891625e9
# Parent  17fc92d33c245c5715ff8cf8d5abf8b5b8ddff0f
improved ATP error handling some more

diff -r 17fc92d33c24 -r 9069e1ad1527 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Thu Jul 29 00:28:57 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu Jul 29 09:41:49 2010 +0200
@@ -87,7 +87,7 @@
 
 val known_perl_failures =
   [(NoPerl, "env: perl"),
-   (NoLibwwwPerl, "HTTP")]
+   (NoLibwwwPerl, "Can't locate HTTP")]
 
 (* named provers *)
 
@@ -201,10 +201,9 @@
   case bash_output "\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of
     (answer, 0) => split_lines answer
   | (answer, _) =>
-    error ("Failed to get available systems at SystemOnTPTP:\n" ^
-           (case known_failure_in_output answer known_perl_failures of
-              SOME failure => string_for_failure failure
-            | NONE => perhaps (try (unsuffix "\n")) answer))
+    error (case known_failure_in_output answer known_perl_failures of
+             SOME failure => string_for_failure failure
+           | NONE => perhaps (try (unsuffix "\n")) answer ^ ".")
 
 fun refresh_systems_on_tptp () =
   Synchronized.change systems (fn _ => get_systems ())
diff -r 17fc92d33c24 -r 9069e1ad1527 src/HOL/Tools/ATP/scripts/remote_atp
--- a/src/HOL/Tools/ATP/scripts/remote_atp	Thu Jul 29 00:28:57 2010 +0200
+++ b/src/HOL/Tools/ATP/scripts/remote_atp	Thu Jul 29 09:41:49 2010 +0200
@@ -96,13 +96,15 @@
 
 #catch errors / failure
 if(!$Response->is_success) {
-  print "HTTP-Error: " . $Response->message . "\n";
+  my $message = $Response->message;
+  $message =~ s/ \(Bad hostname ['"][^'"]*['"]\)//;
+  print $message . "\n";
   exit(-1);
 } elsif (exists($Options{'w'})) {
   print $Response->content;
   exit (0);
 } elsif ($Response->content =~ /WARNING: (\S*) does not exist/) {
-  print "Specified system $1 does not exist\n";
+  print "The ATP \"$1\" is not available at SystemOnTPTP\n";
   exit(-1);
 } else {
   print $Response->content;