# HG changeset patch
# User blanchet
# Date 1276525040 -7200
# Node ID e856582fe9c46ce677c8bcf04d8c18a8212f2f46
# Parent  8cd75d103af9cd86f08ff87f1abd3d4c7b77bc96
improve ATP-specific error messages

diff -r 8cd75d103af9 -r e856582fe9c4 src/HOL/Tools/ATP_Manager/atp_manager.ML
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Mon Jun 14 15:10:50 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Mon Jun 14 16:17:20 2010 +0200
@@ -34,8 +34,8 @@
      axiom_clauses: (thm * (string * int)) list option,
      filtered_clauses: (thm * (string * int)) list option}
   datatype failure =
-    Unprovable | TimedOut | OutOfResources | OldSpass | MalformedInput |
-    MalformedOutput | UnknownError
+    Unprovable | IncompleteUnprovable | TimedOut | OutOfResources | OldSpass |
+    MalformedInput | MalformedOutput | UnknownError
   type prover_result =
     {outcome: failure option,
      message: string,
@@ -95,8 +95,8 @@
    filtered_clauses: (thm * (string * int)) list option};
 
 datatype failure =
-  Unprovable | TimedOut | OutOfResources | OldSpass | MalformedInput |
-  MalformedOutput | UnknownError
+  Unprovable | IncompleteUnprovable | TimedOut | OutOfResources | OldSpass |
+  MalformedInput | MalformedOutput | UnknownError
 
 type prover_result =
   {outcome: failure option,
diff -r 8cd75d103af9 -r e856582fe9c4 src/HOL/Tools/ATP_Manager/atp_systems.ML
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Mon Jun 14 15:10:50 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Mon Jun 14 16:17:20 2010 +0200
@@ -87,6 +87,8 @@
   | (failure :: _) => ("", SOME failure)
 
 fun string_for_failure Unprovable = "The ATP problem is unprovable."
+  | string_for_failure IncompleteUnprovable =
+    "The ATP cannot prove the problem."
   | string_for_failure TimedOut = "Timed out."
   | string_for_failure OutOfResources = "The ATP ran out of resources."
   | string_for_failure OldSpass =
@@ -337,10 +339,11 @@
      \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_generous_secs timeout),
    proof_delims = [("Here is a proof", "Formulae used in the proof")],
    known_failures =
-     [(Unprovable, "SPASS beiseite: Completion found"),
+     [(IncompleteUnprovable, "SPASS beiseite: Completion found"),
       (TimedOut, "SPASS beiseite: Ran out of time"),
       (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
-      (MalformedInput, "Undefined symbol")],
+      (MalformedInput, "Undefined symbol"),
+      (MalformedInput, "Free Variable")],
    max_axiom_clauses = 40,
    prefers_theory_relevant = true}
 val spass = dfg_prover "spass" spass_config