equal
deleted
inserted
replaced
12 |
12 |
13 fun run id ({pre, timeout, log, ...}: Mirabelle.run_args) = |
13 fun run id ({pre, timeout, log, ...}: Mirabelle.run_args) = |
14 if Mirabelle.can_apply timeout Arith_Data.arith_tac pre |
14 if Mirabelle.can_apply timeout Arith_Data.arith_tac pre |
15 then log (arith_tag id ^ "succeeded") |
15 then log (arith_tag id ^ "succeeded") |
16 else () |
16 else () |
17 handle TimeLimit.TimeOut => log (arith_tag id ^ "timeout") |
17 handle Timeout.TIMEOUT _ => log (arith_tag id ^ "timeout") |
18 |
18 |
19 fun invoke _ = Mirabelle.register (init, Mirabelle.catch arith_tag run, done) |
19 fun invoke _ = Mirabelle.register (init, Mirabelle.catch arith_tag run, done) |
20 |
20 |
21 end |
21 end |