src/Pure/ML-Systems/multithreading_polyml.ML
changeset 24668 4058b7b0925c
parent 24297 a50cdc42798d
child 24672 f311717d1f03
     1.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Thu Sep 20 20:56:54 2007 +0200
     1.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Thu Sep 20 20:58:40 2007 +0200
     1.3 @@ -10,8 +10,9 @@
     1.4  signature MULTITHREADING =
     1.5  sig
     1.6    include MULTITHREADING
     1.7 -  val uninterruptible: (Thread.threadAttribute list -> 'a -> 'b) -> 'a -> 'b
     1.8 -  val interruptible: (Thread.threadAttribute list -> 'a -> 'b) -> 'a -> 'b
     1.9 +  val ignore_interrupt: ('a -> 'b) -> 'a -> 'b
    1.10 +  val raise_interrupt: ('a -> 'b) -> 'a -> 'b
    1.11 +  val interrupt_timeout: Time.time -> ('a -> 'b) -> 'a -> 'b
    1.12  end;
    1.13  
    1.14  structure Multithreading: MULTITHREADING =
    1.15 @@ -59,12 +60,28 @@
    1.16        handle Interrupt => (restore (); Exn.Exn Interrupt))
    1.17    end;
    1.18  
    1.19 +
    1.20 +(* interrupt handling *)
    1.21 +
    1.22  fun uninterruptible f x = with_attributes
    1.23    [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptDefer] f x;
    1.24  
    1.25  fun interruptible f x = with_attributes
    1.26    [Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce] f x;
    1.27  
    1.28 +fun ignore_interrupt f = uninterruptible (fn _ => f);
    1.29 +fun raise_interrupt f = interruptible (fn _ => f);
    1.30 +
    1.31 +fun interrupt_timeout time f x =
    1.32 +  uninterruptible (fn atts => fn () =>
    1.33 +    let
    1.34 +      val worker = Thread.self ();
    1.35 +      val watchdog = Thread.fork (interruptible (fn _ => fn () =>
    1.36 +        (OS.Process.sleep time; Thread.interrupt worker)), []);
    1.37 +      val result = Exn.capture (with_attributes atts (fn _ => f)) x;
    1.38 +      val _ = Thread.interrupt watchdog handle Thread _ => ();
    1.39 +    in Exn.release result end) ();
    1.40 +
    1.41  
    1.42  (* critical section -- may be nested within the same thread *)
    1.43  
    1.44 @@ -206,7 +223,7 @@
    1.45  
    1.46  val NAMED_CRITICAL = Multithreading.NAMED_CRITICAL;
    1.47  val CRITICAL = Multithreading.CRITICAL;
    1.48 +val ignore_interrupt = Multithreading.ignore_interrupt;
    1.49 +val raise_interrupt = Multithreading.raise_interrupt;
    1.50 +val interrupt_timeout = Multithreading.interrupt_timeout;
    1.51  
    1.52 -fun ignore_interrupt f = Multithreading.uninterruptible (fn _ => f);
    1.53 -fun raise_interrupt f = Multithreading.interruptible (fn _ => f);
    1.54 -