mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-19 09:12:34 +03:00
47c2de3148
A common issue for users is that the behaviour of the various repl commands are not documented anywhere despite some of them having complex behaviour (e.g. `:set` which accepts a specific set of options). This implements the ability to call `:?|:h|:help` on repl commands to request detailed help for a specific repl command, while preserving the behaviour that calling the help command without any arguments prints the general help text. Generic help is defined as the first line of the help text. Detailed help is defined as the entire help text. This means that `:help :t`, for example, does not error (there is no detailed help) but instead just prints the single line of help text. * [ repl ] Use unlines for detailed help (see #2087) Ideally, the lines affected should be multiline strings. But for some arcane reason, newlines in those get swallowed in Nix and Windows **CI** only Ô.o This was already documented in issue #2087. * [ new ] --except for golden testing lib To allow CI to pass despite #2087 Co-authored-by: Guillaume Allais <guillaume.allais@ens-lyon.org>
127 lines
4.1 KiB
Plaintext
127 lines
4.1 KiB
Plaintext
Main> Set an option
|
|
eval specify what evaluation mode to use:
|
|
typecheck|tc
|
|
normalise|normalize|normal
|
|
execute|exec
|
|
scheme
|
|
|
|
editor specify the name of the editor command
|
|
|
|
cg specify the codegen/backend to use
|
|
builtin codegens are:
|
|
chez
|
|
racket
|
|
refc
|
|
node
|
|
|
|
showimplicits enable displaying implicit arguments as part of the
|
|
output
|
|
|
|
shownamespace enable displaying namespaces as part of the output
|
|
|
|
showmachinenames enable displaying machine names as part of the
|
|
output
|
|
|
|
showtypes enable displaying the type of the term as part of
|
|
the output
|
|
|
|
profile
|
|
|
|
evaltiming enable timing how long evaluation takes and
|
|
displaying this before the printing of the output
|
|
Main> Set an option
|
|
eval specify what evaluation mode to use:
|
|
typecheck|tc
|
|
normalise|normalize|normal
|
|
execute|exec
|
|
scheme
|
|
|
|
editor specify the name of the editor command
|
|
|
|
cg specify the codegen/backend to use
|
|
builtin codegens are:
|
|
chez
|
|
racket
|
|
refc
|
|
node
|
|
|
|
showimplicits enable displaying implicit arguments as part of the
|
|
output
|
|
|
|
shownamespace enable displaying namespaces as part of the output
|
|
|
|
showmachinenames enable displaying machine names as part of the
|
|
output
|
|
|
|
showtypes enable displaying the type of the term as part of
|
|
the output
|
|
|
|
profile
|
|
|
|
evaltiming enable timing how long evaluation takes and
|
|
displaying this before the printing of the output
|
|
Main> Set an option
|
|
eval specify what evaluation mode to use:
|
|
typecheck|tc
|
|
normalise|normalize|normal
|
|
execute|exec
|
|
scheme
|
|
|
|
editor specify the name of the editor command
|
|
|
|
cg specify the codegen/backend to use
|
|
builtin codegens are:
|
|
chez
|
|
racket
|
|
refc
|
|
node
|
|
|
|
showimplicits enable displaying implicit arguments as part of the
|
|
output
|
|
|
|
shownamespace enable displaying namespaces as part of the output
|
|
|
|
showmachinenames enable displaying machine names as part of the
|
|
output
|
|
|
|
showtypes enable displaying the type of the term as part of
|
|
the output
|
|
|
|
profile
|
|
|
|
evaltiming enable timing how long evaluation takes and
|
|
displaying this before the printing of the output
|
|
Main> Set an option
|
|
eval specify what evaluation mode to use:
|
|
typecheck|tc
|
|
normalise|normalize|normal
|
|
execute|exec
|
|
scheme
|
|
|
|
editor specify the name of the editor command
|
|
|
|
cg specify the codegen/backend to use
|
|
builtin codegens are:
|
|
chez
|
|
racket
|
|
refc
|
|
node
|
|
|
|
showimplicits enable displaying implicit arguments as part of the
|
|
output
|
|
|
|
shownamespace enable displaying namespaces as part of the output
|
|
|
|
showmachinenames enable displaying machine names as part of the
|
|
output
|
|
|
|
showtypes enable displaying the type of the term as part of
|
|
the output
|
|
|
|
profile
|
|
|
|
evaltiming enable timing how long evaluation takes and
|
|
displaying this before the printing of the output
|
|
Main>
|
|
Bye for now!
|