IO.Async.File

Reexports

Definitions

data RawMode : Type

  Opaque flag indicating that stdin has been set to
  raw input mode.

Totality: total
Visibility: export
Constructor: 

RM : RawMode

Hint: 

ELift1 World f => Resource f RawMode

toErrno : FileError -> Errno

  Converts a `System.File.Error.FileError` to a POSIX error code

Totality: total
Visibility: export

fileIO : Has Errno es => IO (Either FileError a) -> Async e es a

  Wraps an `IO` action from `System.File` in base by converting
  file errors to POSIX error codes.

Totality: total
Visibility: export

rawMode : Has Errno es => Async e es RawMode

  Enables raw (unbuffered) input mode for stdin.
  
  To make sure this is properly reset when the application ends,
  wrap this in a call to `use` or `use1`:
  
  ```idris
  use1 rawMode $ \_ => your_code
  ```

Totality: total
Visibility: export

withFile : Has Errno es => String -> Flags -> Mode -> (Fd -> Async e es a) -> Async e es a

Totality: total
Visibility: export

readFile : Has Errno es => (0 r : Type) -> FromBuf r => String -> Bits32 -> Async e es r

  Reads up to the given number of bytes from a file.

Totality: total
Visibility: export

writeFile : Has Errno es => ToBuf r => String -> r -> Async e es ()

  Writes a value to an existing file.

Totality: total
Visibility: export

createFile : Has Errno es => ToBuf r => String -> Mode -> r -> Async e es ()

  Writes a value to a file, creating it, if it does not yet exist.

Totality: total
Visibility: export

appendFile : Has Errno es => ToBuf r => String -> Mode -> r -> Async e es ()

  Appends a value to a file.
  
  The file is created if it does not yet exist.

Totality: total
Visibility: export