author | boehmes |
Wed, 07 Apr 2010 20:38:11 +0200 | |
changeset 36082 | 8f10b0e77d94 |
parent 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 |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
14 |
val t1 = start_timing () |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
15 |
val x = f () |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
16 |
val t2 = #message (end_timing t1) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
17 |
val _ = writeln ((report_space ()) ^ "--> "^t2) |
25218 | 18 |
in |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
19 |
x |
25218 | 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 |