Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/Isabelle/Pure/System/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 1 kB

Quelle message_channel.ML Sprache: SML

(*  Title:      Pure/System/message_channel.ML
    Author:     Makarius

Preferably asynchronous channel for Isabelle messages.
*)

signature MESSAGE_CHANNEL =
sig
  type T
  val shutdown: T -> unit
  val message: T -> string -> Properties.T -> XML.body list -> unit
  val make: BinIO.outstream -> T
end;

structure Message_Channel: MESSAGE_CHANNEL =
struct

datatype message = Shutdown | Message of XML.body list;

datatype T = Message_Channel of {mbox: message Mailbox.T, thread: Isabelle_Thread.T};

fun shutdown (Message_Channel {mbox, thread}) =
(Mailbox.send mbox Shutdown;
  Mailbox.await_empty mbox;
  Isabelle_Thread.join thread);

fun message (Message_Channel {mbox, ...}) name props chunks =
  let
    val kind = XML.Encode.string name;
    val props_length = XML.Encode.int (length props);
    val props_chunks = map (XML.Encode.string o Properties.print_eq) props;
  in Mailbox.send mbox (Message (kind :: props_length :: props_chunks @ chunks)) end;

fun make stream =
  let
    val mbox = Mailbox.create ();
    fun loop () = Mailbox.receive NONE mbox |> dispatch
    and dispatch [] = loop ()
      | dispatch (Shutdown :: _) = ()
      | dispatch (Message chunks :: rest) =
          (Byte_Message.write_message_yxml stream chunks; dispatch rest);
    val thread = Isabelle_Thread.fork (Isabelle_Thread.params "message_channel") loop;
  in Message_Channel {mbox = mbox, thread = thread} end;

end;

quality100%

¤ Dauer der Verarbeitung: 0.18 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.