# HG changeset patch
# User blanchet
# Date 1277800596 -7200
# Node ID 1d1754ccd233a516b897982d82313f617dc4dc92
# Parent  1146291fe7186542efb7c7ac6d7efdd64825d1b8
more precise error message for remote ATPs

diff -r 1146291fe718 -r 1d1754ccd233 src/HOL/Tools/ATP_Manager/atp_manager.ML
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Tue Jun 29 10:25:53 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Tue Jun 29 10:36:36 2010 +0200
@@ -33,8 +33,8 @@
      axiom_clauses: ((string * int) * thm) list option,
      filtered_clauses: ((string * int) * thm) list option}
   datatype failure =
-    Unprovable | IncompleteUnprovable | TimedOut | OutOfResources | OldSpass |
-    MalformedInput | MalformedOutput | UnknownError
+    Unprovable | IncompleteUnprovable | CantConnect | TimedOut |
+    OutOfResources | OldSpass | MalformedInput | MalformedOutput | UnknownError
   type prover_result =
     {outcome: failure option,
      message: string,
@@ -102,8 +102,8 @@
    filtered_clauses: ((string * int) * thm) list option}
 
 datatype failure =
-  Unprovable | IncompleteUnprovable | TimedOut | OutOfResources | OldSpass |
-  MalformedInput | MalformedOutput | UnknownError
+  Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources |
+  OldSpass | MalformedInput | MalformedOutput | UnknownError
 
 type prover_result =
   {outcome: failure option,
diff -r 1146291fe718 -r 1d1754ccd233 src/HOL/Tools/ATP_Manager/atp_systems.ML
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Tue Jun 29 10:25:53 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Tue Jun 29 10:36:36 2010 +0200
@@ -95,6 +95,7 @@
 fun string_for_failure Unprovable = "The ATP problem is unprovable."
   | string_for_failure IncompleteUnprovable =
     "The ATP cannot prove the problem."
+  | string_for_failure CantConnect = "Can't connect to remote ATP."
   | string_for_failure TimedOut = "Timed out."
   | string_for_failure OutOfResources = "The ATP ran out of resources."
   | string_for_failure OldSpass =
@@ -465,7 +466,8 @@
   case bash_output "\"$ISABELLE_ATP_MANAGER/SystemOnTPTP\" -w" of
     (answer, 0) => split_lines answer
   | (answer, _) =>
-    error ("Failed to get available systems at SystemOnTPTP:\n" ^ answer)
+    error ("Failed to get available systems at SystemOnTPTP:\n" ^
+           perhaps (try (unsuffix "\n")) answer)
 
 fun refresh_systems_on_tptp () =
   Synchronized.change systems (fn _ => get_systems ())
@@ -480,7 +482,8 @@
   | SOME sys => sys);
 
 val remote_known_failures =
-  [(TimedOut, "says Timeout"),
+  [(CantConnect, "HTTP-Error"),
+   (TimedOut, "says Timeout"),
    (MalformedOutput, "Remote script could not extract proof")]
 
 fun remote_config atp_prefix args