std.io.read
Functions and types for working with Read
ers.
Types
Allows reading bytes from a
. Generally, reading from a reader
advances its internal cursor. This means that multiple read
calls
with the same arguments usually do not return the same value.
Wraps a reader to provide buffering. Buffering is more efficient when performing many small reads, because it avoids many costly reads from the underlying reader.
If you are reading all data at once, buffering is not necessary.
Values
Tries to read num_bytes
byte from the reader. If the reader
has reached end of file or num_bytes
was zero, None
will be returned. Otherwise, an array containing as many bytes as could be
read will be returned. The length of the array is guaranteed to be in the
range [1, num_bytes]
.
Reaching end of file means that this reader will most likely not produce more bytes. It may produce more in the future.
let read_to_end ?read : forall a . [Read a] -> a -> IO (Array Byte)
Read all bytes until end of file is encountered.
let read_to_string reader : forall a . [Read a] -> a -> IO (Option String)
Read all bytes until end of file is encountered into a String
. Returns None
if the read bytes are not valid UTF-8.
let default_read_to_end read : forall a . (a -> Int -> IO (Option (Array Byte))) -> a -> IO (Array Byte)
Constructs a read_to_end
function from a read
function. If it is more efficient,
implementors of Read
should provide their own, specialized version.
Wraps reader
in a Buffered
reader to provide buffering.
let buffered_with_capacity capacity reader : forall a . [Read a] -> Int -> a -> Buffered a
Wraps reader
in a Buffered
reader to provide buffering with the specified
buffer capacity.
#[implicit]
let read_buffered : forall r . [Read r] -> Read (Buffered r)
Allows reading bytes from a
. Generally, reading from a reader
advances its internal cursor. This means that multiple read
calls
with the same arguments usually do not return the same value.
#[implicit]
let disposable_buffered : forall r . [Disposable r] -> Disposable (Buffered r)
A resource that has to be released after use, for example a file handle or a database connection.