Idris2Doc : System

System

Reexports

importpublic Data.So
importpublic System.Escape

Definitions

sleep : HasIOio=>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 slighly 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 : HasIOio=> (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 : HasIOio=>io (ListString)
  Retrieve the arguments to the program call, if there were any.

Totality: total
Visibility: export
enableRawMode : HasIOio=>io (EitherFileError ())
  `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 : HasIOio=>io ()
  `resetRawMode` resets stdin raw mode to original state if
`enableRawMode` had been previously called.

Totality: total
Visibility: export
withRawMode : HasIOio=> (FileError->ioa) -> (() ->ioa) ->ioa
  `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 : HasIOio=>String->io (MaybeString)
  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 : HasIOio=>io (List (String, String))
  Retrieve all the key-value pairs of the environment variables, and return a
list containing them.

Visibility: export
setEnv : HasIOio=>String->String->Bool->ioBool
  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 : HasIOio=>String->ioBool
  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 : HasIOio=>String->ioInt
  Execute a shell command, returning its termination status or -1 if an error
occurred.

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

Visibility: export
run : HasIOio=>ListString->io (String, Int)
Visibility: export
runProcessingOutput : HasIOio=> (String->io ()) ->String->ioInt
  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 : HasIOio=> (String->io ()) ->ListString->ioInt
Visibility: export
time : HasIOio=>ioInteger
  Return the number of seconds since epoch.

Totality: total
Visibility: export
getPID : HasIOio=>ioInt
  Get the ID of the currently running process.

Totality: total
Visibility: export
dataExitCode : 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.
exitWith : HasIOio=>ExitCode->ioa
  Exit the program normally, with the specified status.

Totality: total
Visibility: export
exitFailure : HasIOio=>ioa
  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 : HasIOio=>ioa
  Exit the program after a successful run.

Totality: total
Visibility: export
die : HasIOio=>String->ioa
  Print the error message and call exitFailure

Totality: total
Visibility: export