--- a/src/HOL/Mirabelle/Tools/mirabelle_metis.ML Fri Sep 04 13:57:56 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_metis.ML Sat Sep 05 11:45:57 2009 +0200
@@ -5,7 +5,12 @@
structure Mirabelle_Metis : MIRABELLE_ACTION =
struct
-fun metis_action {pre, post, timeout, log} =
+fun metis_tag id = "#" ^ string_of_int id ^ " metis: "
+
+fun init _ = I
+fun done _ _ = ()
+
+fun run id {pre, post, timeout, log} =
let
val thms = Mirabelle.theorems_of_sucessful_proof post
val names = map Thm.get_name thms
@@ -16,12 +21,13 @@
fun metis ctxt = MetisTools.metis_tac ctxt (thms @ facts)
in
(if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed")
- |> prefix "metis: "
+ |> prefix (metis_tag id)
|> add_info
|> log
end
- handle TimeLimit.TimeOut => log "metis: timeout"
+ handle TimeLimit.TimeOut => log (metis_tag id ^ "timeout")
+ | ERROR msg => log (metis_tag id ^ "error: " ^ msg)
-fun invoke _ = Mirabelle.register (Mirabelle.catch "metis: " metis_action)
+fun invoke _ = Mirabelle.register (init, Mirabelle.catch metis_tag run, done)
end