25218
|
1 |
structure Report =
|
|
2 |
struct
|
|
3 |
|
|
4 |
local
|
|
5 |
|
|
6 |
val report_depth = ref 0
|
|
7 |
fun space n = if n <= 0 then "" else (space (n-1))^" "
|
|
8 |
fun report_space () = space (!report_depth)
|
|
9 |
|
|
10 |
in
|
|
11 |
|
|
12 |
fun timeit f =
|
|
13 |
let
|
|
14 |
val t1 = start_timing ()
|
|
15 |
val x = f ()
|
|
16 |
val t2 = end_timing t1
|
|
17 |
val _ = writeln ((report_space ()) ^ "--> "^t2)
|
|
18 |
in
|
|
19 |
x
|
|
20 |
end
|
|
21 |
|
|
22 |
fun report s f =
|
|
23 |
let
|
|
24 |
val _ = writeln ((report_space ())^s)
|
|
25 |
val _ = report_depth := !report_depth + 1
|
|
26 |
val x = timeit f
|
|
27 |
val _ = report_depth := !report_depth - 1
|
|
28 |
in
|
|
29 |
x
|
|
30 |
end
|
|
31 |
|
|
32 |
end
|
|
33 |
end |