author | webertj |
Mon, 23 Jan 2006 17:29:52 +0100 | |
changeset 18760 | 97aaecb84afe |
child 18790 | 418131f631fc |
permissions | -rw-r--r-- |
18760 | 1 |
(* Title: Pure/ML-Systems/smlnj-interrupt-timeout.ML |
2 |
ID: $Id$ |
|
3 |
Author: Tjark Weber, Makarius |
|
4 |
Copyright 2006 |
|
5 |
||
6 |
Bounded time execution (similar to SML/NJ's TimeLimit structure). |
|
7 |
*) |
|
8 |
||
9 |
fun interrupt_timeout time f x = |
|
10 |
TimeLimit.timeLimit time f x |
|
11 |
handle TimeLimit.TimeOut => raise SML90.Interrupt; |