changeset 18760 | 97aaecb84afe |
parent 18392 | fdefc3cd45c5 |
child 21295 | 63552bc99cfb |
--- a/src/Pure/ML-Systems/poplogml.ML Mon Jan 23 15:23:31 2006 +0100 +++ b/src/Pure/ML-Systems/poplogml.ML Mon Jan 23 17:29:52 2006 +0100 @@ -269,6 +269,12 @@ end; +(* bounded time execution *) + +(* FIXME proper implementation available? *) +fun interrupt_timeout time f x = + f x; + (** interrupts **) (*Note: may get into race conditions*)