| changeset 30240 | 5b25fee0362c |
| parent 25218 | fcf0f50e478c |
| child 32740 | 9dd0a2f83429 |
| 30239:179ff9cb160b | 30240:5b25fee0362c |
|---|---|
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 = 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 |