author | wenzelm |
Tue, 29 Sep 2009 16:24:36 +0200 | |
changeset 32740 | 9dd0a2f83429 |
parent 30187 | b92b3375e919 |
child 32960 | 69916a850301 |
permissions | -rw-r--r-- |
25218 | 1 |
structure Report = |
2 |
struct |
|
3 |
||
4 |
local |
|
5 |
||
32740 | 6 |
val report_depth = Unsynchronized.ref 0 |
25218 | 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 () |
|
30187
b92b3375e919
end_timing: generalized result -- message plus with explicit time values;
wenzelm
parents:
25218
diff
changeset
|
16 |
val t2 = #message (end_timing t1) |
25218 | 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 |