1.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Thu Jul 29 00:28:57 2010 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu Jul 29 09:41:49 2010 +0200
     1.3 @@ -87,7 +87,7 @@
     1.4  
     1.5  val known_perl_failures =
     1.6    [(NoPerl, "env: perl"),
     1.7 -   (NoLibwwwPerl, "HTTP")]
     1.8 +   (NoLibwwwPerl, "Can't locate HTTP")]
     1.9  
    1.10  (* named provers *)
    1.11  
    1.12 @@ -201,10 +201,9 @@
    1.13    case bash_output "\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of
    1.14      (answer, 0) => split_lines answer
    1.15    | (answer, _) =>
    1.16 -    error ("Failed to get available systems at SystemOnTPTP:\n" ^
    1.17 -           (case known_failure_in_output answer known_perl_failures of
    1.18 -              SOME failure => string_for_failure failure
    1.19 -            | NONE => perhaps (try (unsuffix "\n")) answer))
    1.20 +    error (case known_failure_in_output answer known_perl_failures of
    1.21 +             SOME failure => string_for_failure failure
    1.22 +           | NONE => perhaps (try (unsuffix "\n")) answer ^ ".")
    1.23  
    1.24  fun refresh_systems_on_tptp () =
    1.25    Synchronized.change systems (fn _ => get_systems ())

     2.1 --- a/src/HOL/Tools/ATP/scripts/remote_atp	Thu Jul 29 00:28:57 2010 +0200
     2.2 +++ b/src/HOL/Tools/ATP/scripts/remote_atp	Thu Jul 29 09:41:49 2010 +0200
     2.3 @@ -96,13 +96,15 @@
     2.4  
     2.5  #catch errors / failure
     2.6  if(!$Response->is_success) {
     2.7 -  print "HTTP-Error: " . $Response->message . "\n";
     2.8 +  my $message = $Response->message;
     2.9 +  $message =~ s/ \(Bad hostname ['"][^'"]*['"]\)//;
    2.10 +  print $message . "\n";
    2.11    exit(-1);
    2.12  } elsif (exists($Options{'w'})) {
    2.13    print $Response->content;
    2.14    exit (0);
    2.15  } elsif ($Response->content =~ /WARNING: (\S*) does not exist/) {
    2.16 -  print "Specified system $1 does not exist\n";
    2.17 +  print "The ATP \"$1\" is not available at SystemOnTPTP\n";
    2.18    exit(-1);
    2.19  } else {
    2.20    print $Response->content;