Idris2Doc : System

System

Reexports

import public Data.So
import public System.Escape

Definitions

sleep : HasIO io => Int -> io ()
  Sleep for the specified number of seconds or, if signals are supported,
until an un-ignored signal arrives.
The exact wall-clock time slept might slightly differ depending on how busy
the system is and the resolution of the system's clock.

@ sec the number of seconds to sleep for

Totality: total
Visibility: export
usleep : HasIO io => (usec : Int) -> So (usec >= 0) => io ()
  Sleep for the specified number of microseconds or, if signals are supported,
until an un-ignored signal arrives.
The exact wall-clock time slept might slighly differ depending on how busy
the system is and the resolution of the system's clock.

@ usec the number of microseconds to sleep for

Totality: total
Visibility: export
getArgs : HasIO io => io (List String)
  Retrieve the arguments to the program call, if there were any.

Totality: total
Visibility: export
enableRawMode : HasIO io => io (Either FileError ())
  `enableRawMode` enables raw mode for stdin, allowing characters
to be read one at a time, without buffering or echoing.
If `enableRawMode` is used, the program should call `resetRawMode` before
exiting. Consider using `withRawMode` instead to ensure the tty is reset.

This is not supported on windows.

Totality: total
Visibility: export
resetRawMode : HasIO io => io ()
  `resetRawMode` resets stdin raw mode to original state if
`enableRawMode` had been previously called.

Totality: total
Visibility: export
withRawMode : HasIO io => (FileError -> io a) -> (() -> io a) -> io a
  `withRawMode` performs a given operation after setting stdin to raw mode
and ensure that stdin is reset to its original state afterwards.

This is not supported on windows.

Totality: total
Visibility: export
getEnv : HasIO io => String -> io (Maybe String)
  Retrieve the specified environment variable's value string, or `Nothing` if
there is no such environment variable.

@ var the name of the environment variable to look up

Totality: total
Visibility: export
getEnvironment : HasIO io => io (List (String, String))
  Retrieve all the key-value pairs of the environment variables, and return a
list containing them.

Visibility: export
setEnv : HasIO io => String -> String -> Bool -> io Bool
  Add the specified variable with the given value string to the environment,
optionally overwriting any existing environment variable with the same name.
Returns True whether the value is set, overwritten, or not overwritten because
overwrite was False. Returns False if a system error occurred. You can `getErrno`
to check the error.

@ var the name of the environment variable to set
@ val the value string to set the environment variable to
@ overwrite whether to overwrite the existing value if an environment
variable with the specified name already exists

Totality: total
Visibility: export
unsetEnv : HasIO io => String -> io Bool
  Delete the specified environment variable. Returns `True` either if the
value was deleted or if the value was not defined/didn't exist. Returns
`False` if a system error occurred. You can `getErrno` to check the error.

Totality: total
Visibility: export
system : HasIO io => String -> io Int
  Execute a shell command, returning its termination status or -1 if an error
occurred.

Totality: total
Visibility: export
system : HasIO io => List String -> io Int
Totality: total
Visibility: export
run : HasIO io => String -> io (String, Int)
  Run a shell command, returning its stdout, and exit code.

Visibility: export
run : HasIO io => List String -> io (String, Int)
Visibility: export
runProcessingOutput : HasIO io => (String -> io ()) -> String -> io Int
  Run a shell command, allowing processing its stdout line by line.

Notice that is the line of the command ends with a newline character,
it will be present in the string passed to the processing function.

This function returns an exit code which value should be consistent with the `run` function.

Visibility: export
runProcessingOutput : HasIO io => (String -> io ()) -> List String -> io Int
Visibility: export
time : HasIO io => io Integer
  Return the number of seconds since epoch.

Totality: total
Visibility: export
getPID : HasIO io => io Int
  Get the ID of the currently running process.

Totality: total
Visibility: export
data ExitCode : Type
  Programs can either terminate successfully, or end in a caught
failure.

Totality: total
Visibility: public export
Constructors:
ExitSuccess : ExitCode
  Terminate successfully.
ExitFailure : (errNo : Int) -> So (not (errNo == 0)) => ExitCode
  Program terminated for some prescribed reason.

@errNo A non-zero numerical value indicating failure.
@prf Proof that the int value is non-zero.

Hints:
Cast Int ExitCode
Cast ExitCode Int
exitWith : HasIO io => ExitCode -> io a
  Exit the program normally, with the specified status.

Totality: total
Visibility: export
exitFailure : HasIO io => io a
  Exit the program with status value 1, indicating failure.
If you want to specify a custom status value, see `exitWith`.

Totality: total
Visibility: export
exitSuccess : HasIO io => io a
  Exit the program after a successful run.

Totality: total
Visibility: export
die : HasIO io => String -> io a
  Print the error message and call exitFailure

Totality: total
Visibility: export