--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Jun 08 08:47:43 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Jun 08 08:47:43 2011 +0200
@@ -16,7 +16,7 @@
string -> params -> bool -> int -> int -> Proof.state
-> ((string * locality) * thm list) list
-> ((string * locality) * thm list) list option
- * ((unit -> play) * (play -> string))
+ * ((unit -> play) * (play -> string) * string)
val run_minimize :
params -> int -> (Facts.ref * Attrib.src list) list -> Proof.state -> unit
end;
@@ -167,7 +167,7 @@
Int.min (msecs, Time.toMilliseconds time + slack_msecs)
|> Time.fromMilliseconds
val facts = filter_used_facts used_facts facts
- val (min_thms, {preplay, message, ...}) =
+ val (min_thms, {preplay, message, message_tail, ...}) =
if length facts >= Config.get ctxt binary_min_facts then
binary_minimize (do_test new_timeout) facts
else
@@ -178,17 +178,18 @@
(case length (filter (curry (op =) Chained o snd o fst) min_thms) of
0 => ""
| n => " (including " ^ string_of_int n ^ " chained)") ^ ".")
- in (SOME min_thms, (preplay, message)) end
+ in (SOME min_thms, (preplay, message, message_tail)) end
| {outcome = SOME TimedOut, preplay, ...} =>
(NONE,
(preplay,
fn _ => "Timeout: You can increase the time limit using the \
\\"timeout\" option (e.g., \"timeout = " ^
- string_of_int (10 + msecs div 1000) ^ "\")."))
+ string_of_int (10 + msecs div 1000) ^ "\").",
+ ""))
| {preplay, message, ...} =>
- (NONE, (preplay, prefix "Prover error: " o message)))
+ (NONE, (preplay, prefix "Prover error: " o message, "")))
handle ERROR msg =>
- (NONE, (K (Failed_to_Play Metis), fn _ => "Error: " ^ msg))
+ (NONE, (K (Failed_to_Play Metis), fn _ => "Error: " ^ msg, ""))
end
fun run_minimize (params as {provers, ...}) i refs state =
@@ -207,8 +208,9 @@
| prover :: _ =>
(kill_provers ();
minimize_facts prover params false i n state facts
- |> (fn (_, (preplay, message)) =>
- Output.urgent_message (message (preplay ()))))
+ |> (fn (_, (preplay, message, message_tail)) =>
+ message (preplay ()) ^ message_tail
+ |> Output.urgent_message))
end
end;