--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Aug 13 10:29:49 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Aug 13 11:34:56 2013 +0200
@@ -16,7 +16,7 @@
type play = Sledgehammer_Reconstructor.play
type minimize_command = Sledgehammer_Reconstructor.minimize_command
- datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize
+ datatype mode = Auto_Try | Try | Normal | Normal_Result | MaSh | Auto_Minimize | Minimize
type params =
{debug : bool,
@@ -161,7 +161,7 @@
(** The Sledgehammer **)
-datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize
+datatype mode = Auto_Try | Try | Normal | Normal_Result | MaSh | Auto_Minimize | Minimize
(* Identifier that distinguishes Sledgehammer from other tools that could use
"Async_Manager". *)
@@ -667,6 +667,7 @@
fun suffix_of_mode Auto_Try = "_try"
| suffix_of_mode Try = "_try"
| suffix_of_mode Normal = ""
+ | suffix_of_mode Normal_Result = ""
| suffix_of_mode MaSh = ""
| suffix_of_mode Auto_Minimize = "_min"
| suffix_of_mode Minimize = "_min"
@@ -930,7 +931,7 @@
(output, run_time, used_from, atp_proof, outcome)) =
with_cleanup clean_up run () |> tap export
val important_message =
- if mode = Normal andalso
+ if (mode = Normal orelse mode = Normal_Result) andalso
random_range 0 (atp_important_message_keep_quotient - 1) = 0 then
extract_important_message output
else
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue Aug 13 10:29:49 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue Aug 13 11:34:56 2013 +0200
@@ -157,7 +157,7 @@
state |> Proof.map_context
(Config.put sledgehammer_result (quote name ^ ": " ^ message ()))
else
- ((if outcome_code = someN orelse mode = Normal then
+ ((if outcome_code = someN orelse mode = Normal orelse mode = Normal_Result then
quote name ^ ": " ^ message ()
else
"")
@@ -294,7 +294,7 @@
|> Par_List.map (fn f => ignore (f (unknownN, state)))
handle ERROR msg => (print ("Error: " ^ msg); error msg)
fun maybe f (accum as (outcome_code, _)) =
- accum |> (mode = Normal orelse outcome_code <> someN) ? f
+ accum |> (mode = Normal orelse mode = Normal_Result orelse outcome_code <> someN) ? f
in
(unknownN, state)
|> (if blocking then