src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML

 *)
 
 structure Mirabelle_Quickcheck : MIRABELLE_ACTION =
 struct
 
-fun quickcheck_action args {pre, timeout, log, ...} =
+fun qc_tag id = "#" ^ string_of_int id ^ " quickcheck: "
+
+fun init _ = I
+fun done _ _ = ()
+
+fun run args id {pre, timeout, log, ...} =
   let
     val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst
     val quickcheck = Quickcheck.quickcheck (filter has_valid_key args) 1
   in
     (case TimeLimit.timeLimit timeout quickcheck pre of
-      NONE => log "quickcheck: no counterexample"
-    | SOME _ => log "quickcheck: counterexample found")
+      NONE => log (qc_tag id ^ "no counterexample")
+    | SOME _ => log (qc_tag id ^ "counterexample found"))
   end
-  handle TimeLimit.TimeOut => log "quickcheck: timeout"
+  handle TimeLimit.TimeOut => log (qc_tag id ^ "timeout")
+       | ERROR msg => log (qc_tag id ^ "error: " ^ msg)
 
 fun invoke args =
-  Mirabelle.register (Mirabelle.catch "quickcheck: " (quickcheck_action args))
+  Mirabelle.register (init, Mirabelle.catch qc_tag (run args), done)
 
 end