src/Pure/ML-Systems/multithreading_polyml.ML
changeset 41713 a21084741b37
parent 41710 11ae688e4e30
child 43761 e72ba84ae58f
     1.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Mon Feb 07 23:57:03 2011 +0100
     1.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Tue Feb 08 14:09:24 2011 +0100
     1.3 @@ -45,6 +45,9 @@
     1.4  val no_interrupts =
     1.5    [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptDefer];
     1.6  
     1.7 +val test_interrupts =
     1.8 +  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptSynch];
     1.9 +
    1.10  val public_interrupts =
    1.11    [Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce];
    1.12  
    1.13 @@ -61,6 +64,14 @@
    1.14        Thread.InterruptState Thread.InterruptAsynchOnce
    1.15      | x => x);
    1.16  
    1.17 +fun interrupted () =
    1.18 +  let
    1.19 +    val orig_atts = safe_interrupts (Thread.getAttributes ());
    1.20 +    val _ = Thread.setAttributes test_interrupts;
    1.21 +    val test = Exn.capture Thread.testInterrupt ();
    1.22 +    val _ = Thread.setAttributes orig_atts;
    1.23 +  in Exn.release test end;
    1.24 +
    1.25  fun with_attributes new_atts e =
    1.26    let
    1.27      val orig_atts = safe_interrupts (Thread.getAttributes ());