changeset 21297 | 2b60e9b70a8c |
parent 21296 | 3c245a8a5001 |
child 21298 | 6d2306b2376d |
--- a/src/Pure/ML-Systems/smlnj-interrupt-timeout.ML Fri Nov 10 23:22:03 2006 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,11 +0,0 @@ -(* Title: Pure/ML-Systems/smlnj-interrupt-timeout.ML - ID: $Id$ - Author: Tjark Weber, Makarius - Copyright 2006 - -Bounded time execution (similar to SML/NJ's TimeLimit structure). -*) - -fun interrupt_timeout time f x = - TimeLimit.timeLimit time f x - handle TimeLimit.TimeOut => raise Interrupt;