src/Pure/Concurrent/synchronized.ML
changeset 62505 9e2a65912111
parent 59195 f8588372d70e
child 62663 bea354f6ff21
equal deleted inserted replaced
62504:f14f17e656a6 62505:9e2a65912111
    47           (case f x of
    47           (case f x of
    48             NONE =>
    48             NONE =>
    49               (case Multithreading.sync_wait NONE (time_limit x) cond lock of
    49               (case Multithreading.sync_wait NONE (time_limit x) cond lock of
    50                 Exn.Res true => try_change ()
    50                 Exn.Res true => try_change ()
    51               | Exn.Res false => NONE
    51               | Exn.Res false => NONE
    52               | Exn.Exn exn => reraise exn)
    52               | Exn.Exn exn => Exn.reraise exn)
    53           | SOME (y, x') =>
    53           | SOME (y, x') =>
    54               uninterruptible (fn _ => fn () =>
    54               uninterruptible (fn _ => fn () =>
    55                 (var := x'; ConditionVar.broadcast cond; SOME y)) ())
    55                 (var := x'; ConditionVar.broadcast cond; SOME y)) ())
    56         end;
    56         end;
    57     in try_change () end);
    57     in try_change () end);