equal
deleted
inserted
replaced
11 fun done _ _ = () |
11 fun done _ _ = () |
12 |
12 |
13 fun times_ten time = Time.fromMilliseconds (10 * Time.toMilliseconds time) |
13 fun times_ten time = Time.fromMilliseconds (10 * Time.toMilliseconds time) |
14 |
14 |
15 fun run id ({pre, timeout, log, ...}: Mirabelle.run_args) = |
15 fun run id ({pre, timeout, log, ...}: Mirabelle.run_args) = |
16 if TimeLimit.timeLimit (times_ten timeout) (Try0.try0 (SOME timeout) ([], [], [], [])) pre |
16 if Timeout.apply (times_ten timeout) (Try0.try0 (SOME timeout) ([], [], [], [])) pre |
17 then log (try0_tag id ^ "succeeded") |
17 then log (try0_tag id ^ "succeeded") |
18 else () |
18 else () |
19 handle TimeLimit.TimeOut => log (try0_tag id ^ "timeout") |
19 handle Timeout.TIMEOUT _ => log (try0_tag id ^ "timeout") |
20 |
20 |
21 fun invoke _ = Mirabelle.register (init, Mirabelle.catch try0_tag run, done) |
21 fun invoke _ = Mirabelle.register (init, Mirabelle.catch try0_tag run, done) |
22 |
22 |
23 end |
23 end |