Idris2Doc : System.File.Buffer

System.File.Buffer

(source)

Reexports

importpublic System.File.Error
importpublic System.File.Types

Definitions

readBufferData : HasIOio=>File->Buffer->Int->Int->io (EitherFileErrorInt)
  Read the data from the file into the given buffer.

@ fh the file handle to read from
@ buf the buffer to read the data into
@ offset the position in buffer to start adding
@ maxbytes the maximum size to read; must not exceed buffer length

Totality: total
Visibility: export
writeBufferData : HasIOio=>File->Buffer->Int->Int->io (Either (FileError, Int) ())
  Write the data from the buffer to the given `File`. Returns the number
of bytes that have been written upon a write error. Otherwise, it can
be assumed that `size` number of bytes have been written.
(If you do not have a `File` and just want to write to a file at a known
path, you probably want to use `writeBufferToFile`.)

@ fh the file handle to write to
@ buf the buffer from which to get the data to write
@ offset the position in buffer to write from
@ size the number of bytes to write; must not exceed buffer length

Totality: total
Visibility: export
writeBufferToFile : HasIOio=>String->Buffer->Int->io (Either (FileError, Int) ())
  Attempt to write the data from the buffer to the file at the specified file
name. Returns the number of bytes that have been written upon a write error.
Otherwise, it can be assumed that `size` number of bytes have been written.

@ fn the file name to write to
@ buf the buffer from which to get the data to write
@ size the number of bytes to write; must not exceed buffer length

Totality: total
Visibility: export
createBufferFromFile : HasIOio=>String->io (EitherFileErrorBuffer)
  Create a new buffer by opening a file and reading its contents into a new
buffer whose size matches the file size.

@ fn the name of the file to read

Totality: total
Visibility: export