src/Pure/ML-Systems/multithreading_polyml.ML
changeset 32286 1fb5db48002d
parent 32230 9f6461b1c9cc
child 32295 400cc493d466
     1.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Thu Jul 30 18:43:52 2009 +0200
     1.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Thu Jul 30 23:06:06 2009 +0200
     1.3 @@ -110,6 +110,9 @@
     1.4      val _ = Thread.setAttributes orig_atts;
     1.5    in Exn.release result end;
     1.6  
     1.7 +
     1.8 +(* regular interruptibility *)
     1.9 +
    1.10  fun interruptible f x =
    1.11    (Thread.testInterrupt (); with_attributes regular_interrupts (fn _ => fn x => f x) x);
    1.12  
    1.13 @@ -118,6 +121,29 @@
    1.14      f (fn g => with_attributes atts (fn _ => fn y => g y)) x);
    1.15  
    1.16  
    1.17 +(* synchronous wait *)
    1.18 +
    1.19 +fun sync_attributes e =
    1.20 +  let
    1.21 +    val orig_atts = Thread.getAttributes ();
    1.22 +    val broadcast =
    1.23 +      (case List.find (fn Thread.EnableBroadcastInterrupt _ => true | _ => false) orig_atts of
    1.24 +        NONE => Thread.EnableBroadcastInterrupt false
    1.25 +      | SOME att => att);
    1.26 +    val interrupt_state =
    1.27 +      (case List.find (fn Thread.InterruptState _ => true | _ => false) orig_atts of
    1.28 +        NONE => Thread.InterruptState Thread.InterruptDefer
    1.29 +      | SOME (state as Thread.InterruptState Thread.InterruptDefer) => state
    1.30 +      | _ => Thread.InterruptState Thread.InterruptSynch);
    1.31 +  in with_attributes [broadcast, interrupt_state] (fn _ => fn () => e ()) () end;
    1.32 +
    1.33 +fun sync_wait time cond lock =
    1.34 +  sync_attributes (fn () =>
    1.35 +    (case time of
    1.36 +      SOME t => ConditionVar.waitUntil (cond, lock, t)
    1.37 +    | NONE => (ConditionVar.wait (cond, lock); true)));
    1.38 +
    1.39 +
    1.40  (* execution with time limit *)
    1.41  
    1.42  structure TimeLimit =
    1.43 @@ -192,8 +218,9 @@
    1.44  
    1.45      val _ = while ! result = Wait do
    1.46        restore_attributes (fn () =>
    1.47 -        (ConditionVar.waitUntil (result_cond, result_mutex, Time.now () + Time.fromMilliseconds 100); ())
    1.48 -          handle Exn.Interrupt => kill 10) ();
    1.49 +        (ignore (sync_wait (SOME (Time.+ (Time.now (), Time.fromMilliseconds 100)))
    1.50 +            result_cond result_mutex)
    1.51 +          handle Exn.Interrupt => kill 10)) ();
    1.52  
    1.53      (*cleanup*)
    1.54      val output = read_file output_name handle IO.Io _ => "";
    1.55 @@ -269,5 +296,5 @@
    1.56  
    1.57  end;
    1.58  
    1.59 -structure BasicMultithreading: BASIC_MULTITHREADING = Multithreading;
    1.60 -open BasicMultithreading;
    1.61 +structure Basic_Multithreading: BASIC_MULTITHREADING = Multithreading;
    1.62 +open Basic_Multithreading;