Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/ML-Systems/smlnj-interrupt-timeout.ML
author wenzelm
Wed, 13 Sep 2006 21:41:31 +0200
changeset 20531 7de9caf4fd78
parent 18790 418131f631fc
permissions -rw-r--r--
added exists_type;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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;















isabelle