equal
deleted
inserted
replaced
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); |