Type of dropbox holding a value of type 'a

The exception returned when trying to access a 'closed' dropbox.

Create an empty dropbox.

put t e puts the element e inside the dropbox t. If the dropbox already held an element, the old element is discarded and replaced by the new one.

• raises Closed

  if close t has been called.

take t is a promise that resolves as soon as an element is held by t. The element is removed from t when the promise resolves.

If t already holds an element when take t is called, the promise resolves immediately. Otherwise, the promise resolves when an element is put there.

• raises Closed

  if close t has been called.

take_with_timeout timeout t behaves like take t except that it returns None if timeout resolves before an element is put.

Note that timeout is canceled (i.e., fails with Canceled) if an element is put in time (or if one is already present).

• raises Closed

  if close t has been called.

peek t is Some e if t holds e and None if t does not hold any element.

• raises Closed

  if close t has been called.

close t closes the dropbox t. It terminates all the waiting reader with the exception Closed. All further read or write will also immediately fail with Closed, except if the dropbox is not empty when close is called. In that case, a single (and last) take will succeed.