Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: mailbox.ML Sprache: SML

Original von: Isabelle^©

(*  Title:      Pure/Concurrent/mailbox.ML
    Author:     Makarius

Message exchange via mailbox, with multiple senders (non-blocking,
unbounded buffering) and single receiver (bulk messages).
*)

signature MAILBOX =
sig
  type 'a T
  val create: unit -> 'a T
  val send: 'a T -> 'a -> unit
  val receive: Time.time option -> 'a T -> 'a list
  val await_empty: 'a T -> unit
end;

structure Mailbox: MAILBOX =
struct

datatype 'a T = Mailbox of 'a list Synchronized.var;

fun create () = Mailbox (Synchronized.var "mailbox" []);

fun send (Mailbox mailbox) msg = Synchronized.change mailbox (cons msg);

fun receive timeout (Mailbox mailbox) =
  Synchronized.timed_access mailbox
    (fn _ => Option.map (fn t => Time.now () + t) timeout)
    (fn [] => NONE | msgs => SOME (msgs, []))
  |> these |> rev;

fun await_empty (Mailbox mailbox) =
  Synchronized.guarded_access mailbox (fn [] => SOME ((), []) | _ => NONE);

end;

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.