mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-12-23 04:42:05 +03:00
ae841108ef
This ignores empty lines in the REPL and doesn't show a parse error on CTRL+D/EOF anymore. Add NOP variant to REPLCmd to represent an empty command. Split command in eoi or nonEmptyCommand. nonEmptyCommand is still guaranteed to consume input. command may be eoi in which case it does not consume input. Print a newline after receiving EOF on the console. Since this is only relevant in the REPL (quiet or not) this uses putStrLn rather than iputStrLn. |
||
|---|---|---|
| .. | ||
| Elab | ||
| IDEMode | ||
| Socket | ||
| CommandLine.idr | ||
| Desugar.idr | ||
| Error.idr | ||
| Main.idr | ||
| ModTree.idr | ||
| Package.idr | ||
| Parser.idr | ||
| ProcessIdr.idr | ||
| REPL.idr | ||
| REPLCommon.idr | ||
| REPLOpts.idr | ||
| Resugar.idr | ||
| SetOptions.idr | ||
| Socket.idr | ||
| Syntax.idr | ||