--- a/src/HOL/Mirabelle/Tools/mirabelle.ML Wed May 12 12:22:44 2021 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML Wed May 12 13:10:13 2021 +0200
@@ -68,15 +68,15 @@
)
-fun log_exn log tag id e = log (tag id ^ "exception:\n" ^ General.exnMessage e)
+fun exn_log tag id e = tag id ^ "exception:\n" ^ General.exnMessage e
-fun catch tag f id (st as {log, ...}: run_args) = (f id st; ())
+fun catch tag f id (args: run_args) = f id args
handle exn =>
- if Exn.is_interrupt exn then Exn.reraise exn else (log_exn log tag id exn; ())
+ if Exn.is_interrupt exn then Exn.reraise exn else #log args (exn_log tag id exn)
-fun catch_result tag d f id (st as {log, ...}: run_args) = f id st
+fun catch_result tag default f id (args: run_args) = f id args
handle exn =>
- if Exn.is_interrupt exn then Exn.reraise exn else (log_exn log tag id exn; d)
+ if Exn.is_interrupt exn then Exn.reraise exn else (#log args (exn_log tag id exn); default)
fun register (init, run, done) thy =
let val id = length (Actions.get thy) + 1