| changeset 50255 | d0ec1f0d1d7d |
| child 50280 | 0eb9b5d09f31 |
| 50254:935ac0ad7e83 | 50255:d0ec1f0d1d7d |
|---|---|
1 (* Title: Pure/ML/ml_statistics_dummy.ML |
|
2 Author: Makarius |
|
3 |
|
4 ML runtime statistics -- dummy version. |
|
5 *) |
|
6 |
|
7 signature ML_STATISTICS = |
|
8 sig |
|
9 val enabled: bool Unsynchronized.ref |
|
10 val get: unit -> Properties.T |
|
11 end; |
|
12 |
|
13 structure ML_Statistics: ML_STATISTICS = |
|
14 struct |
|
15 |
|
16 val enabled = Unsynchronized.ref false; |
|
17 fun get () = []; |
|
18 |
|
19 end; |
|
20 |