# HG changeset patch
# User blanchet
# Date 1271862386 -7200
# Node ID 25e69e93954d1964ec4110fc4a43b0635a9803c1
# Parent  9a7c5b86a1052d95d04d532e35c1b91e32c6d4e8
failure of reconstructing the Isar proof (e.g., exception) should not prevent Sledgehammer from showing the short one-liner proof -- but in "debug" mode we do want to know what the exception is

diff -r 9a7c5b86a105 -r 25e69e93954d src/HOL/Tools/ATP_Manager/atp_minimal.ML
--- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Wed Apr 21 16:38:03 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Wed Apr 21 17:06:26 2010 +0200
@@ -84,7 +84,7 @@
 
 (* minimalization of thms *)
 
-fun minimize_theorems (params as {minimize_timeout, isar_proof, modulus,
+fun minimize_theorems (params as {debug, minimize_timeout, isar_proof, modulus,
                                   sorts, ...})
                       prover atp_name i state name_thms_pairs =
   let
@@ -122,7 +122,7 @@
             ["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^ ".")
         in
           (SOME min_thms,
-           proof_text isar_proof modulus sorts ctxt (K "") proof
+           proof_text isar_proof debug modulus sorts ctxt (K "") proof
                       internal_thm_names goal i |> fst)
         end
     | (Timeout, _) =>
diff -r 9a7c5b86a105 -r 25e69e93954d src/HOL/Tools/ATP_Manager/atp_wrapper.ML
--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Wed Apr 21 16:38:03 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Wed Apr 21 17:06:26 2010 +0200
@@ -188,7 +188,7 @@
       (prepare_clauses higher_order false)
       (write_tptp_file (debug andalso overlord andalso not isar_proof)) command
       (arguments timeout) known_failures
-      (proof_text (supports_isar_proofs andalso isar_proof) modulus sorts)
+      (proof_text (supports_isar_proofs andalso isar_proof) debug modulus sorts)
       name params minimize_command
 
 fun tptp_prover name p = (name, generic_tptp_prover (name, p));
diff -r 9a7c5b86a105 -r 25e69e93954d src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Wed Apr 21 16:38:03 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Wed Apr 21 17:06:26 2010 +0200
@@ -20,10 +20,10 @@
     minimize_command -> string -> string vector -> thm -> int
     -> string * string list
   val isar_proof_text:
-    int -> bool -> Proof.context -> minimize_command -> string -> string vector
-    -> thm -> int -> string * string list
+    bool -> int -> bool -> Proof.context -> minimize_command -> string
+    -> string vector -> thm -> int -> string * string list
   val proof_text:
-    bool -> int -> bool -> Proof.context -> minimize_command -> string
+    bool -> bool -> int -> bool -> Proof.context -> minimize_command -> string
     -> string vector -> thm -> int -> string * string list
 end;
 
@@ -555,7 +555,8 @@
     (metis_line i n xs ^ minimize_line minimize_command xs, kill_chained lemmas)
   end
 
-fun isar_proof_text modulus sorts ctxt minimize_command proof thm_names goal i =
+fun isar_proof_text debug modulus sorts ctxt minimize_command proof thm_names
+                    goal i =
   let
     (* We could use "split_lines", but it can return blank lines. *)
     val lines = String.tokens (equal #"\n");
@@ -566,17 +567,22 @@
     val (one_line_proof, lemma_names) =
       metis_proof_text minimize_command proof thm_names goal i
     val tokens = String.tokens (fn c => c = #" ") one_line_proof
+    fun isar_proof_for () =
+      case isar_proof_from_tstp_file cnfs modulus sorts ctxt goal i thm_names of
+        "" => ""
+      | isar_proof => Markup.markup Markup.sendback isar_proof
     val isar_proof =
-      if member (op =) tokens chained_hint then ""
-      else isar_proof_from_tstp_file cnfs modulus sorts ctxt goal i thm_names
-  in
-    (one_line_proof ^
-     (if isar_proof = "" then ""
-      else "\nStructured proof:\n" ^ Markup.markup Markup.sendback isar_proof),
-     lemma_names)
-  end
+      if member (op =) tokens chained_hint then
+        ""
+      else if debug then
+        isar_proof_for ()
+      else
+        try isar_proof_for ()
+        |> the_default "Error: The Isar proof reconstruction failed."
+  in (one_line_proof ^ isar_proof, lemma_names) end
 
-fun proof_text isar_proof modulus sorts ctxt =
-  if isar_proof then isar_proof_text modulus sorts ctxt else metis_proof_text
+fun proof_text isar_proof debug modulus sorts ctxt =
+  if isar_proof then isar_proof_text debug modulus sorts ctxt
+  else metis_proof_text
 
 end;