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: exportchangeDir : HasIO io => String -> io Bool
Change the current working directory to the specified path. Returns whether
the operation succeeded.
Totality: total
Visibility: exportcurrentDir : HasIO io => io (Maybe String)
Get the absolute path of the current working directory. Returns `Nothing` if
an error occurred.
Totality: total
Visibility: exportopenDir : HasIO io => String -> io (Either FileError Directory)
Try to open the directory at the specified path.
Totality: total
Visibility: exportcloseDir : HasIO io => Directory -> io ()
Close the given `Directory`.
Totality: total
Visibility: exportremoveDir : HasIO io => String -> io ()
Remove the directory at the specified path.
If the directory is not empty, this operation fails.
Totality: total
Visibility: exportnextDirEntry : HasIO io => Directory -> io (Either FileError (Maybe String))
Get the next entry in the `Directory`, omitting the '.' and '..' entries.
Totality: total
Visibility: exportlistDir : 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