|Copyright||(c) The University of Glasgow 2008|
|Portability||non-portable (GHC Extensions)|
Class of buffered IO devices
The purpose of
BufferedIO is to provide a common interface for I/O devices that can read and write data through a buffer. Devices that implement
BufferedIO include ordinary files, memory-mapped files, and bytestrings. The underlying device implementing a
Handle must provide
allocate a new buffer. The size of the buffer is at the discretion of the device; e.g. for a memory-mapped file the buffer will probably cover the entire file.
reads bytes into the buffer, blocking if there are no bytes available. Returns the number of bytes read (zero indicates end-of-file), and the new buffer.
reads bytes into the buffer without blocking. Returns the number of bytes read (Nothing indicates end-of-file), and the new buffer.
Prepares an empty write buffer. This lets the device decide how to set up a write buffer: the buffer may need to point to a specific location in memory, for example. This is typically used by the client when switching from reading to writing on a buffered read/write device.
There is no corresponding operation for read buffers, because before reading the client will always call
Flush all the data from the supplied write buffer out to the device. The returned buffer should be empty, and ready for writing.
Flush data from the supplied write buffer out to the device without blocking. Returns the number of bytes written and the remaining buffer.
© The University of Glasgow and others
Licensed under a BSD-style license (see top of the page).