src/Pure/ML-Systems/polyml-interrupt-timeout.ML
author wenzelm
Tue, 24 Jul 2007 19:44:33 +0200
changeset 23962 e0358fac0541
parent 21266 288a504c24d6
child 24651 452962f294a3
permissions -rw-r--r--
Runtime exceptions as values (from library.ML);
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/polyml-interrupt-timeout.ML
97aaecb84afe TimeLimit replaced by interrupt_timeout
webertj
parents:
diff changeset
     2
    ID:         $Id$
21266
288a504c24d6 new CCS-based implementation that should work with PolyML 5.0
webertj
parents: 18814
diff changeset
     3
    Author:     Tjark Weber
18760
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) for Poly/ML.
97aaecb84afe TimeLimit replaced by interrupt_timeout
webertj
parents:
diff changeset
     7
*)
97aaecb84afe TimeLimit replaced by interrupt_timeout
webertj
parents:
diff changeset
     8
21266
288a504c24d6 new CCS-based implementation that should work with PolyML 5.0
webertj
parents: 18814
diff changeset
     9
(* Note: This code may cause an infrequent segmentation fault (due to a race
288a504c24d6 new CCS-based implementation that should work with PolyML 5.0
webertj
parents: 18814
diff changeset
    10
         condition between process creation/termination and garbage collection)
288a504c24d6 new CCS-based implementation that should work with PolyML 5.0
webertj
parents: 18814
diff changeset
    11
         before PolyML 5.0. *)
18760
97aaecb84afe TimeLimit replaced by interrupt_timeout
webertj
parents:
diff changeset
    12
21266
288a504c24d6 new CCS-based implementation that should work with PolyML 5.0
webertj
parents: 18814
diff changeset
    13
(* Note: f must not manipulate the timer used by Posix.Process.sleep *)
18814
1a904aebfef0 interrupt_timeout for Poly replaced by stub
webertj
parents: 18760
diff changeset
    14
1a904aebfef0 interrupt_timeout for Poly replaced by stub
webertj
parents: 18760
diff changeset
    15
fun interrupt_timeout time f x =
21266
288a504c24d6 new CCS-based implementation that should work with PolyML 5.0
webertj
parents: 18814
diff changeset
    16
let
288a504c24d6 new CCS-based implementation that should work with PolyML 5.0
webertj
parents: 18814
diff changeset
    17
  val ch = Process.channel ()
288a504c24d6 new CCS-based implementation that should work with PolyML 5.0
webertj
parents: 18814
diff changeset
    18
  val interrupt_timer = Process.console (fn () =>
288a504c24d6 new CCS-based implementation that should work with PolyML 5.0
webertj
parents: 18814
diff changeset
    19
    (Posix.Process.sleep time; Process.send (ch, NONE)))
288a504c24d6 new CCS-based implementation that should work with PolyML 5.0
webertj
parents: 18814
diff changeset
    20
  val interrupt_worker = Process.console (fn () =>
288a504c24d6 new CCS-based implementation that should work with PolyML 5.0
webertj
parents: 18814
diff changeset
    21
    Process.send (ch, SOME (capture f x)))
288a504c24d6 new CCS-based implementation that should work with PolyML 5.0
webertj
parents: 18814
diff changeset
    22
in
288a504c24d6 new CCS-based implementation that should work with PolyML 5.0
webertj
parents: 18814
diff changeset
    23
  case Process.receive ch of
288a504c24d6 new CCS-based implementation that should work with PolyML 5.0
webertj
parents: 18814
diff changeset
    24
    NONE    => (interrupt_worker (); raise Interrupt)
288a504c24d6 new CCS-based implementation that should work with PolyML 5.0
webertj
parents: 18814
diff changeset
    25
  | SOME fx => (interrupt_timer (); release fx)
288a504c24d6 new CCS-based implementation that should work with PolyML 5.0
webertj
parents: 18814
diff changeset
    26
end;