equal
deleted
inserted
replaced
50 |
50 |
51 val limit = Time.+ (Time.now (), timeout); |
51 val limit = Time.+ (Time.now (), timeout); |
52 fun check () = not (Queue.is_empty (! messages)) orelse |
52 fun check () = not (Queue.is_empty (! messages)) orelse |
53 ConditionVar.waitUntil (cond, lock, limit) andalso check (); |
53 ConditionVar.waitUntil (cond, lock, limit) andalso check (); |
54 val ok = restore_attributes check () |
54 val ok = restore_attributes check () |
55 handle Interrupt => (Mutex.unlock lock; raise Interrupt); |
55 handle Exn.Interrupt => (Mutex.unlock lock; raise Exn.Interrupt); |
56 val res = if ok then SOME (change_result messages Queue.dequeue) else NONE; |
56 val res = if ok then SOME (change_result messages Queue.dequeue) else NONE; |
57 |
57 |
58 val _ = Mutex.unlock lock; |
58 val _ = Mutex.unlock lock; |
59 in res end) (); |
59 in res end) (); |
60 |
60 |