# HG changeset patch
# User boehmes
# Date 1251575826 -7200
# Node ID 8f0dc876fb1b76aed35ea7acc01a4d7f2d6cab25
# Parent  6b93b73a712b1c8dd5ab77586306cf9355b85c8b
propagate theorem names, in addition to generated return message

diff -r 6b93b73a712b -r 8f0dc876fb1b src/HOL/Tools/ATP_Manager/atp_manager.ML
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Fri Aug 28 19:57:12 2009 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Sat Aug 29 21:57:06 2009 +0200
@@ -24,7 +24,7 @@
   type prover = int -> (thm * (string * int)) list option ->
     (thm * (string * int)) list option -> string -> int ->
     Proof.context * (thm list * thm) ->
-    bool * string * string * string vector * (thm * (string * int)) list
+    bool * (string * string list) * string * string vector * (thm * (string * int)) list
   val add_prover: string -> prover -> theory -> theory
   val print_provers: theory -> unit
   val get_prover: string -> theory -> prover option
@@ -305,7 +305,7 @@
 type prover = int -> (thm * (string * int)) list option ->
   (thm * (string * int)) list option -> string -> int ->
   Proof.context * (thm list * thm) ->
-  bool * string * string * string vector * (thm * (string * int)) list
+  bool * (string * string list) * string * string vector * (thm * (string * int)) list
 
 fun err_dup_prover name = error ("Duplicate prover: " ^ quote name);
 
@@ -345,7 +345,7 @@
           let
             val _ = register birthtime deadtime (Thread.self (), desc)
             val result =
-              let val (success, message, _, _, _) =
+              let val (success, (message, _), _, _, _) =
                 prover (get_timeout ()) NONE NONE name i (Proof.get_goal proof_state)
               in (success, message) end
               handle ResHolClause.TOO_TRIVIAL
diff -r 6b93b73a712b -r 8f0dc876fb1b src/HOL/Tools/ATP_Manager/atp_wrapper.ML
--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Fri Aug 28 19:57:12 2009 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Sat Aug 29 21:57:06 2009 +0200
@@ -89,10 +89,10 @@
     val failure = find_failure proof
     val success = rc = 0 andalso is_none failure
     val message =
-      if is_some failure then "External prover failed."
-      else if rc <> 0 then "External prover failed: " ^ proof
-      else "Try this command: " ^
-        produce_answer name (proof, thm_names, conj_pos, ctxt, th, subgoalno)
+      if is_some failure then ("External prover failed.", [])
+      else if rc <> 0 then ("External prover failed: " ^ proof, [])
+      else apfst (fn s => "Try this command: " ^ s)
+        (produce_answer name (proof, thm_names, conj_pos, ctxt, th, subgoalno))
     val _ = Output.debug (fn () => "Sledgehammer response (rc = " ^ string_of_int rc ^ "):\n" ^ proof)
   in (success, message, proof, thm_names, the_filtered_clauses) end;
 
diff -r 6b93b73a712b -r 8f0dc876fb1b src/HOL/Tools/res_reconstruct.ML
--- a/src/HOL/Tools/res_reconstruct.ML	Fri Aug 28 19:57:12 2009 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML	Sat Aug 29 21:57:06 2009 +0200
@@ -17,10 +17,10 @@
   (* extracting lemma list*)
   val find_failure: string -> string option
   val lemma_list: bool -> string ->
-    string * string vector * (int * int) * Proof.context * Thm.thm * int -> string
+    string * string vector * (int * int) * Proof.context * Thm.thm * int -> string * string list
   (* structured proofs *)
   val structured_proof: string ->
-    string * string vector * (int * int) * Proof.context * Thm.thm * int -> string
+    string * string vector * (int * int) * Proof.context * Thm.thm * int -> string * string list
 end;
 
 structure ResReconstruct : RES_RECONSTRUCT =
@@ -554,9 +554,10 @@
 
   fun lemma_list dfg name result =
     let val (lemmas, used_conj) = extract_lemmas (get_step_nums dfg) result
-    in sendback_metis_nochained lemmas ^ "\n" ^ minimize_line name lemmas ^
+    in (sendback_metis_nochained lemmas ^ "\n" ^ minimize_line name lemmas ^
       (if used_conj then ""
-       else "\nWarning: Goal is provable because context is inconsistent.")
+       else "\nWarning: Goal is provable because context is inconsistent."),
+       lemmas)
     end;
 
   (* === Extracting structured Isar-proof === *)
@@ -567,11 +568,11 @@
     val nospaces = String.translate (fn c => if Char.isSpace c then "" else str c)
     val proofextract = get_proof_extract proof
     val cnfs = filter (String.isPrefix "cnf(") (map nospaces (lines proofextract))
-    val one_line_proof = lemma_list false name result
+    val (one_line_proof, lemma_names) = lemma_list false name result
     val structured = if chained_hint mem_string (String.tokens (fn c => c = #" ") one_line_proof) then ""
                 else decode_tstp_file cnfs ctxt goal subgoalno thm_names
     in
-    one_line_proof ^ "\n\n" ^ (Markup.markup Markup.sendback) structured
+    (one_line_proof ^ "\n\n" ^ (Markup.markup Markup.sendback) structured, lemma_names)
   end
 
 end;