src/HOL/Mirabelle/Tools/mirabelle.ML

   val start_line : int Config.T
   val end_line : int Config.T
   val setup : theory -> theory
 
   (*core*)
-  type init_action
-  type done_action
-  type run_action
-  type action
+  type init_action = int -> theory -> theory
+  type done_args = {last: Toplevel.state, log: string -> unit}
+  type done_action = int -> done_args -> unit
+  type run_args = {pre: Proof.state, post: Toplevel.state option,
+    timeout: Time.time, log: string -> unit, pos: Position.T}
+  type run_action = int -> run_args -> unit
+  type action = init_action * run_action * done_action
   val catch : (int -> string) -> run_action -> run_action
   val register : action -> theory -> theory
   val step_hook : Toplevel.transition -> Toplevel.state -> Toplevel.state ->
     unit
 

 
 
 (* Mirabelle core *)
 
 type init_action = int -> theory -> theory
-type done_action = int -> {last: Toplevel.state, log: string -> unit} -> unit
-type run_action = int -> {pre: Proof.state, post: Toplevel.state option,
-  timeout: Time.time, log: string -> unit, pos: Position.T} -> unit
+type done_args = {last: Toplevel.state, log: string -> unit}
+type done_action = int -> done_args -> unit
+type run_args = {pre: Proof.state, post: Toplevel.state option,
+  timeout: Time.time, log: string -> unit, pos: Position.T}
+type run_action = int -> run_args -> unit
 type action = init_action * run_action * done_action
 
 structure Actions = TheoryDataFun
 (
   type T = (int * run_action * done_action) list

 
 
 fun app_with f g x = (g x; ())
   handle (exn as Exn.Interrupt) => reraise exn | exn => (f exn; ())
 
-fun catch tag f id (st as {log, ...}) =
+fun catch tag f id (st as {log, ...}: run_args) =
   let fun log_exn e = log (tag id ^ "exception:\n" ^ General.exnMessage e)
   in app_with log_exn (f id) st end
 
 fun register (init, run, done) thy =
   let val id = length (Actions.get thy) + 1