changeset 24688 | a5754ca5c510 |
child 29564 | f8b933a62151 |
24687:f24306b9e073 | 24688:a5754ca5c510 |
---|---|
1 (* Title: Pure/ML-Systems/time_limit.ML |
|
2 ID: $Id$ |
|
3 Author: Makarius |
|
4 |
|
5 Dummy implementation of NJ's TimeLimit structure. |
|
6 *) |
|
7 |
|
8 signature TIME_LIMIT = |
|
9 sig |
|
10 exception TimeOut |
|
11 val timeLimit : Time.time -> ('a -> 'b) -> 'a -> 'b |
|
12 end; |
|
13 |
|
14 structure TimeLimit: TIME_LIMIT = |
|
15 struct |
|
16 |
|
17 exception TimeOut; |
|
18 fun timeLimit _ f x = f x; |
|
19 |
|
20 end; |
|
21 |