Idris2Doc : System.Directory

System.Directory

Directory access and handling.

Reexports

importpublic System.File

Definitions

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

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

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

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

Totality: total
Visibility: export
openDir : HasIOio=>String->io (EitherFileErrorDirectory)
  Try to open the directory at the specified path.

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

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

Totality: total
Visibility: export
nextDirEntry : HasIOio=>Directory->io (EitherFileError (MaybeString))
  Get the next entry in the `Directory`, omitting the '.' and '..' entries.

Totality: total
Visibility: export
listDir : HasIOio=>String->io (EitherFileError (ListString))
  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