# HG changeset patch
# User blanchet
# Date 1306188093 -7200
# Node ID 1403595ec38cd3e7a38ccbd5880fd289307c7e48
# Parent  bf45fd2488a2760cd44b54d579325dd0d38300cd
slightly gracefuller handling of LEO-II and Satallax output

diff -r bf45fd2488a2 -r 1403595ec38c src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Tue May 24 00:01:33 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Tue May 24 00:01:33 2011 +0200
@@ -12,6 +12,8 @@
   type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula
   type 'a problem = 'a ATP_Problem.problem
 
+  exception UNRECOGNIZED_ATP_PROOF of unit
+
   datatype failure =
     Unprovable |
     IncompleteUnprovable |
@@ -66,6 +68,8 @@
 
 open ATP_Problem
 
+exception UNRECOGNIZED_ATP_PROOF of unit
+
 datatype failure =
   Unprovable |
   IncompleteUnprovable |
@@ -445,7 +449,7 @@
   s |> strip_spaces_except_between_ident_chars
     |> raw_explode
     |> Scan.finite Symbol.stopper
-           (Scan.error (!! (fn _ => raise Fail "unrecognized ATP output")
+           (Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ())
                            (Scan.repeat1 (parse_line problem))))
     |> fst
 
diff -r bf45fd2488a2 -r 1403595ec38c src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue May 24 00:01:33 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue May 24 00:01:33 2011 +0200
@@ -385,9 +385,9 @@
      " -t " ^ string_of_int (Int.min (max_remote_secs, (to_secs 0 timeout)))
      ^ " -s " ^ the_system system_name system_versions,
    proof_delims = union (op =) tstp_proof_delims proof_delims,
-   known_failures =
-     known_failures @ known_perl_failures @
+   known_failures = known_failures @ known_perl_failures @
      [(Unprovable, "says Satisfiable"),
+      (ProofMissing, "says Theorem"),
       (IncompleteUnprovable, "says Unknown"),
       (IncompleteUnprovable, "says GaveUp"),
       (TimedOut, "says Timeout"),
diff -r bf45fd2488a2 -r 1403595ec38c src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue May 24 00:01:33 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue May 24 00:01:33 2011 +0200
@@ -610,6 +610,7 @@
                   extract_tstplike_proof_and_outcome verbose complete res_code
                       proof_delims known_failures output
                   |>> atp_proof_from_tstplike_proof atp_problem
+                  handle UNRECOGNIZED_ATP_PROOF () => ([], SOME ProofIncomplete)
                 val (conjecture_shape, facts_offset, fact_names,
                      typed_helpers) =
                   if is_none outcome then