show what failed to play

--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Jun 06 20:36:34 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Jun 06 20:36:34 2011 +0200
@@ -398,7 +398,7 @@
       | SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))
     fun failed failure =
       ({outcome = SOME failure, used_facts = [], run_time_in_msecs = NONE,
-        preplay = K ATP_Reconstruct.Failed_to_Play,
+        preplay = K (ATP_Reconstruct.Failed_to_Play ATP_Reconstruct.Metis),
         message = K ""}, ~1)
     val ({outcome, used_facts, run_time_in_msecs, preplay, message}
          : Sledgehammer_Provers.prover_result,

--- a/src/HOL/Tools/ATP/atp_reconstruct.ML	Mon Jun 06 20:36:34 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML	Mon Jun 06 20:36:34 2011 +0200
@@ -22,7 +22,7 @@
   datatype play =
     Played of reconstructor * Time.time |
     Trust_Playable of reconstructor * Time.time option|
-    Failed_to_Play
+    Failed_to_Play of reconstructor
 
   type minimize_command = string list -> string
   type one_line_params =
@@ -73,7 +73,7 @@
 datatype play =
   Played of reconstructor * Time.time |
   Trust_Playable of reconstructor * Time.time option |
-  Failed_to_Play
+  Failed_to_Play of reconstructor
 
 type minimize_command = string list -> string
 type one_line_params =
@@ -294,23 +294,22 @@
                          subgoal, subgoal_count) =
   let
     val (chained, extra) = split_used_facts used_facts
-    val (reconstructor, ext_time) =
+    val (failed, reconstructor, ext_time) =
       case preplay of
         Played (reconstructor, time) =>
-        (SOME reconstructor, (SOME (false, time)))
+        (false, reconstructor, (SOME (false, time)))
       | Trust_Playable (reconstructor, time) =>
-        (SOME reconstructor,
+        (false, reconstructor,
          case time of
            NONE => NONE
          | SOME time =>
            if time = Time.zeroTime then NONE else SOME (true, time))
-      | Failed_to_Play => (NONE, NONE)
+      | Failed_to_Play reconstructor => (true, reconstructor, NONE)
     val try_line =
-      case reconstructor of
-        SOME r => ([], map fst extra)
-                  |> reconstructor_command r subgoal subgoal_count
-                  |> try_command_line banner ext_time
-      | NONE => "One-line proof reconstruction failed."
+      ([], map fst extra)
+      |> reconstructor_command reconstructor subgoal subgoal_count
+      |> (if failed then enclose "One-line proof reconstruction failed: " "."
+          else try_command_line banner ext_time)
   in try_line ^ minimize_line minimize_command (map fst (extra @ chained)) end
 
 (** Hard-core proof reconstruction: structured Isar proofs **)
@@ -1103,7 +1102,7 @@
 
 fun proof_text ctxt isar_proof isar_params
                (one_line_params as (preplay, _, _, _, _, _)) =
-  (if isar_proof orelse preplay = Failed_to_Play then
+  (if case preplay of Failed_to_Play _ => true | _ => isar_proof then
      isar_proof_text ctxt isar_proof isar_params
    else
      one_line_proof_text) one_line_params

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Mon Jun 06 20:36:34 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Mon Jun 06 20:36:34 2011 +0200
@@ -185,7 +185,8 @@
                  string_of_int (10 + msecs div 1000) ^ "\")."))
      | {preplay, message, ...} =>
        (NONE, (preplay, prefix "Prover error: " o message)))
-    handle ERROR msg => (NONE, (K Failed_to_Play, fn _ => "Error: " ^ msg))
+    handle ERROR msg =>
+           (NONE, (K (Failed_to_Play Metis), fn _ => "Error: " ^ msg))
   end
 
 fun run_minimize (params as {provers, ...}) i refs state =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Jun 06 20:36:34 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Jun 06 20:36:34 2011 +0200
@@ -429,7 +429,7 @@
 
 fun play_one_line_proof debug timeout ths state i reconstructors =
   let
-    fun play [] [] = Failed_to_Play
+    fun play [] [] = Failed_to_Play (hd reconstructors)
       | play (timed_out :: _) [] = Trust_Playable (timed_out, SOME timeout)
       | play timed_out (reconstructor :: reconstructors) =
         let val timer = Timer.startRealTimer () in
@@ -815,7 +815,7 @@
               end)
         end
       | SOME failure =>
-        ([], K Failed_to_Play, fn _ => string_for_failure failure)
+        ([], K (Failed_to_Play Metis), fn _ => string_for_failure failure)
   in
     {outcome = outcome, used_facts = used_facts, run_time_in_msecs = msecs,
      preplay = preplay, message = message}
@@ -1000,7 +1000,8 @@
                else
                  "")
             end)
-      | SOME failure => (K Failed_to_Play, fn _ => string_for_failure failure)
+      | SOME failure =>
+        (K (Failed_to_Play Metis), fn _ => string_for_failure failure)
   in
     {outcome = outcome, used_facts = used_facts,
      run_time_in_msecs = run_time_in_msecs, preplay = preplay,
@@ -1029,7 +1030,9 @@
                           minimize_command name, subgoal, subgoal_count)
                     in one_line_proof_text one_line_params end}
     | play =>
-      let val failure = if play = Failed_to_Play then GaveUp else TimedOut in
+      let
+        val failure = case play of Failed_to_Play _ => GaveUp | _ => TimedOut
+      in
         {outcome = SOME failure, used_facts = [], run_time_in_msecs = NONE,
          preplay = K play, message = fn _ => string_for_failure failure}
       end