Idris2Doc : FS.Posix

FS.Posix

(source)

Reexports

import public IO.Async.Posix
import public FS
import public System.Posix.Dir
import public System.Posix.File.Stats
import public System.Posix.File.Type
import public System.Posix.File

Definitions

record Entry : PathType -> Type
Totality: total
Visibility: public export
Constructor: 
E : Path p -> FileType -> FileStats -> Entry p

Projections:
.path : Entry p -> Path p
.stats : Entry p -> FileStats
.type : Entry p -> FileType

Hints:
Eq (Entry p)
Show (Entry p)
.path : Entry p -> Path p
Totality: total
Visibility: public export
path : Entry p -> Path p
Totality: total
Visibility: public export
.type : Entry p -> FileType
Totality: total
Visibility: public export
type : Entry p -> FileType
Totality: total
Visibility: public export
.stats : Entry p -> FileStats
Totality: total
Visibility: public export
stats : Entry p -> FileStats
Totality: total
Visibility: public export
hidden : Entry p -> Bool
  True if the given directory entry is hidden.

Totality: total
Visibility: export
regular : Entry p -> Bool
  True if the given directory entry is a regular file

Totality: total
Visibility: export
regularExt : Body -> Entry p -> Bool
  True if the given directory entry is a regular file
with the given extension.

Totality: total
Visibility: export
entries_ : Has Errno es => Bool -> Dir -> AsyncStream e es String
  Produces a stream of directory entries.

This is a low-level utility to just emit the content of a directory.
Use `entries` to get proper file paths and information about the types
and stats of files.

Totality: total
Visibility: export
entries : Has Errno es => Path p -> AsyncStream e es (Entry p)
  Produces a stream of directory entries.

This will not include the parent directory `".."` in the output.

Totality: total
Visibility: export
deepEntries : Has Errno es => Path p -> AsyncStream e es (Entry p)
  Like entries but also enters child directories.

Totality: total
Visibility: export
bytesRaw : PollH e => Has Errno es => FileDesc a => a -> Buf -> AsyncStream e es EMBuffer
  Streams chunks of bytes into a pre-allocated buffer.

This uses non-blocking I/O, so it can also be used for reading from pipes
such as standard input.

Totality: total
Visibility: export
bytes : PollH e => Has Errno es => FileDesc a => a -> Bits32 -> AsyncStream e es ByteString
  Streams chunks of byte of at most the given size from the given
file descriptor.

This uses non-blocking I/O, so it can also be used for reading from pipes
such as standard input.

Totality: total
Visibility: export
bytesPtr : PollH e => Has Errno es => FileDesc a => a -> CPtr -> AsyncStream e es ByteString
  Like `bytes` but allows us to reuse a pre-allocated C-pointer.

Totality: total
Visibility: export
readBytes : PollH e => Has Errno es => {default 65535 _ : Bits32} -> String -> AsyncStream e es ByteString
  Tries to open the given file and starts reading chunks of bytes
from the created file descriptor.

Totality: total
Visibility: export
readRawBytes : PollH e => Has Errno es => Buf -> String -> AsyncStream e es EMBuffer
  Tries to open the given file and starts reading chunks of bytes
from the created file descriptor.

Totality: total
Visibility: export
content : PollH e => Has Errno es => Entry p -> AsyncStream e es ByteString
  Streams the content of a directory entry

Totality: total
Visibility: export
writeTo : PollH e => Has Errno es => ToBuf o => FileDesc a => a -> AsyncPull e o es r -> AsyncPull e Void es r
Totality: total
Visibility: export
printLnTo : PollH e => Has Errno es => Show o => FileDesc a => a -> AsyncPull e o es r -> AsyncPull e Void es r
Totality: total
Visibility: export
printLnsTo : PollH e => Has Errno es => Show o => FileDesc a => a -> AsyncPull e (List o) es r -> AsyncPull e Void es r
Totality: total
Visibility: export
printTo : PollH e => Has Errno es => Show o => FileDesc a => a -> AsyncPull e o es r -> AsyncPull e Void es r
Totality: total
Visibility: export
writeFile : PollH e => Has Errno es => ToBuf o => String -> AsyncPull e o es r -> AsyncPull e Void es r
Totality: total
Visibility: export
appendFile : PollH e => Has Errno es => ToBuf o => String -> AsyncPull e o es r -> AsyncPull e Void es r
Totality: total
Visibility: export