# HG changeset patch
# User blanchet
# Date 1300810853 -3600
# Node ID 889d767ce5f47b9d412f9aa83676534a4ea35ce9
# Parent  83f3dc509068b336574aab054476c50cfbbd739e
make Minimizer honor "verbose" and "debug" options better

diff -r 83f3dc509068 -r 889d767ce5f4 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Tue Mar 22 12:49:07 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Tue Mar 22 17:20:53 2011 +0100
@@ -32,8 +32,8 @@
   val extract_known_failure :
     (failure * string) list -> string -> failure option
   val extract_tstplike_proof_and_outcome :
-    bool -> bool -> int -> (string * string) list -> (failure * string) list
-    -> string -> string * failure option
+    bool -> bool -> bool -> int -> (string * string) list
+    -> (failure * string) list -> string -> string * failure option
   val is_same_step : step_name * step_name -> bool
   val atp_proof_from_tstplike_string : bool -> string -> string proof
   val map_term_names_in_atp_proof :
@@ -80,7 +80,10 @@
   else
     s
 fun short_output verbose output =
-  if verbose then elide_string 1000 output else ""
+  if verbose then
+    if output = "" then "No details available" else elide_string 1000 output
+  else
+    ""
 
 val missing_message_tail =
   " appears to be missing. You will need to install it if you want to invoke \
@@ -154,17 +157,19 @@
   |> find_first (fn (_, pattern) => String.isSubstring pattern output)
   |> Option.map fst
 
-fun extract_tstplike_proof_and_outcome verbose complete res_code proof_delims
-                                       known_failures output =
+fun extract_tstplike_proof_and_outcome debug verbose complete res_code
+                                       proof_delims known_failures output =
   case extract_known_failure known_failures output of
-    NONE => (case extract_tstplike_proof proof_delims output of
-             "" => ("", SOME (if res_code = 0 andalso output = "" then
-                                ProofMissing
-                              else
-                                UnknownError (short_output verbose output)))
-           | tstplike_proof =>
-             if res_code = 0 then (tstplike_proof, NONE)
-             else ("", SOME (UnknownError (short_output verbose output))))
+    NONE =>
+    (case extract_tstplike_proof proof_delims output of
+       "" =>
+       ("", SOME (if res_code = 0 andalso (not debug orelse output = "") then
+                    ProofMissing
+                  else
+                    UnknownError (short_output verbose output)))
+     | tstplike_proof =>
+       if res_code = 0 then (tstplike_proof, NONE)
+       else ("", SOME (UnknownError (short_output verbose output))))
   | SOME failure =>
     ("", SOME (if failure = IncompleteUnprovable andalso complete then
                  Unprovable
diff -r 83f3dc509068 -r 889d767ce5f4 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Tue Mar 22 12:49:07 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Tue Mar 22 17:20:53 2011 +0100
@@ -62,7 +62,7 @@
                       (concl_t :: hyp_ts @ maps (map prop_of o snd) facts))
         end
     val params =
-      {debug = debug, verbose = false, overlord = overlord, blocking = true,
+      {debug = debug, verbose = verbose, overlord = overlord, blocking = true,
        provers = provers, type_sys = type_sys, explicit_apply = explicit_apply,
        relevance_thresholds = (1.01, 1.01), max_relevant = NONE,
        isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
diff -r 83f3dc509068 -r 889d767ce5f4 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Mar 22 12:49:07 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Mar 22 17:20:53 2011 +0100
@@ -403,8 +403,8 @@
                          I)
                   |>> (if measure_run_time then split_time else rpair NONE)
                 val (tstplike_proof, outcome) =
-                  extract_tstplike_proof_and_outcome verbose complete res_code
-                      proof_delims known_failures output
+                  extract_tstplike_proof_and_outcome debug verbose complete
+                      res_code proof_delims known_failures output
               in (output, msecs, tstplike_proof, outcome) end
             val run_twice =
               has_incomplete_mode andalso not auto andalso