|
(* Title: Pure/General/bytes.ML
Author: Makarius
Byte-vector messages.
*)
signature BYTES =
sig
val read_line: BinIO.instream -> string option
val read_block: BinIO.instream -> int -> string
end;
structure Bytes: BYTES =
struct
fun read_line stream =
let
val result = trim_line o String.implode o rev;
fun read cs =
(case BinIO.input1 stream of
NONE => if null cs then NONE else SOME (result cs)
| SOME b =>
(case Byte.byteToChar b of
#"\n" => SOME (result cs)
| c => read (c :: cs)));
in read [] end;
fun read_block stream n =
Byte.bytesToString (BinIO.inputN (stream, n));
end;
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
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.
|
