comma package:Agda
Backend-specific command-line flags. Should at minimum contain a flag
to enable the backend.
The command queue.
This queue should only be manipulated by
initialiseCommandQueue and maybeAbort.
Commands that should be processed, in the order in which they should
be processed. Each command is associated with a number, and the
numbers are strictly increasing. Abort commands are not put on this
queue.
Opposite of
liftIO for
CommandM.
This function should only be applied to computations that are
guaranteed not to raise any errors (except for
IOExceptions).
Returns the command line options which are currently in effect.
For the sake of flexibility, we parametrize interactive commands with
an arbitrary string payload, e.g. to allow extra user input, or have
backends provide multiple commands with a single record field.
A generalised command type.
Auxiliary state of an interactive computation.
The type of top-level backend interactive commmands.
The type of top-level backend interactive commmands.