isabelle: src/Pure/ML-Systems/smlnj-interrupt-timeout.ML@1a904aebfef0 (annotated)

18760 97aaecb84afe TimeLimit replaced by interrupt_timeout webertj parents: diff changeset	1	(* Title: Pure/ML-Systems/smlnj-interrupt-timeout.ML
97aaecb84afe TimeLimit replaced by interrupt_timeout webertj parents: diff changeset	2	ID: $Id$
97aaecb84afe TimeLimit replaced by interrupt_timeout webertj parents: diff changeset	3	Author: Tjark Weber, Makarius
97aaecb84afe TimeLimit replaced by interrupt_timeout webertj parents: diff changeset	4	Copyright 2006
97aaecb84afe TimeLimit replaced by interrupt_timeout webertj parents: diff changeset	5
97aaecb84afe TimeLimit replaced by interrupt_timeout webertj parents: diff changeset	6	Bounded time execution (similar to SML/NJ's TimeLimit structure).
97aaecb84afe TimeLimit replaced by interrupt_timeout webertj parents: diff changeset	7	*)
97aaecb84afe TimeLimit replaced by interrupt_timeout webertj parents: diff changeset	8
97aaecb84afe TimeLimit replaced by interrupt_timeout webertj parents: diff changeset	9	fun interrupt_timeout time f x =
97aaecb84afe TimeLimit replaced by interrupt_timeout webertj parents: diff changeset	10	TimeLimit.timeLimit time f x
18790 418131f631fc interrupt_timeout now raises Interrupt instead of SML90.Interrupt webertj parents: 18760 diff changeset	11	handle TimeLimit.TimeOut => raise Interrupt;