equal
deleted
inserted
replaced
9 |
9 |
10 in |
10 in |
11 |
11 |
12 fun timeit f = |
12 fun timeit f = |
13 let |
13 let |
14 val t1 = start_timing () |
14 val t1 = start_timing () |
15 val x = f () |
15 val x = f () |
16 val t2 = #message (end_timing t1) |
16 val t2 = #message (end_timing t1) |
17 val _ = writeln ((report_space ()) ^ "--> "^t2) |
17 val _ = writeln ((report_space ()) ^ "--> "^t2) |
18 in |
18 in |
19 x |
19 x |
20 end |
20 end |
21 |
21 |
22 fun report s f = |
22 fun report s f = |
23 let |
23 let |
24 val _ = writeln ((report_space ())^s) |
24 val _ = writeln ((report_space ())^s) |