Idris2Doc : System.Directory

System.Directory

Directory access and handling.

Reexports

import public System.File

Definitions

DirPtr : Type
Totality: total
Visibility: public export
data Directory : Type
  Data structure for managing the pointer to a directory.

Totality: total
Visibility: export
Constructor: 
MkDir : DirPtr -> Directory
createDir : HasIO io => String -> io (Either FileError ())
  Try to create a directory at the specified path.

Totality: total
Visibility: export
changeDir : HasIO io => String -> io Bool
  Change the current working directory to the specified path. Returns whether
the operation succeeded.

Totality: total
Visibility: export
currentDir : HasIO io => io (Maybe String)
  Get the absolute path of the current working directory. Returns `Nothing` if
an error occurred.

Totality: total
Visibility: export
openDir : HasIO io => String -> io (Either FileError Directory)
  Try to open the directory at the specified path.

Totality: total
Visibility: export
closeDir : HasIO io => Directory -> io ()
  Close the given `Directory`.

Totality: total
Visibility: export
removeDir : HasIO io => String -> io ()
  Remove the directory at the specified path.
If the directory is not empty, this operation fails.

Totality: total
Visibility: export
nextDirEntry : HasIO io => Directory -> io (Either FileError (Maybe String))
  Get the next entry in the `Directory`, omitting the '.' and '..' entries.

Totality: total
Visibility: export
listDir : HasIO io => String -> io (Either FileError (List String))
  Get a list of all the entries in the directory at the specified path,
excluding the '.' and '..' entries.

@ name the directory to list

Totality: total
Visibility: export