idris-lang/Idris-dev — pull request #1558 by tac-tics (2014-09-28 04:45:35+00:00)
Title: Issue1416

Re: https://github.com/idris-lang/Idris-dev/issues/1416

This should address most of the concerns raised in this issue. Here's a summary of the changes:

`parseCmd` from `Idris.REPLParser` now returns an `Either String Command` instead of a `Command`. The `Left`s are custom error messages to be shown when a user specifies a command (starting with a colon).

The monstrous `pCmd` parser has been tidied up a bit. I grouped as many commands as I could based on the sort of arguments they take. There are a handful of helper functions (`noArgs`, `fnNameArg`, `exprArg`, etc) that handle command dispatch and error handling in a uniform way. For commands that this was not possible, the implementation of the command has been delegated to a named funciton starting with `cmd_` (for instance `cmd_doc`).

The `cmd` helper function has been changed so that it now returns the chosen "spelling" of the command (`c` vs `compile`). All the helper functions and dispatch functions take the spelling as an argument. The argument goes unused in many of the dispatch functions, with the intent they can be updated with better error messages later.

Lastly, the helper parsers (for parsing options, console options, colours, pretty printing, etc) have been made into local definitions near their call sites.

As mentioned above, not all the error handling has been reworked quite yet. But this change should make tweaking error messages and adding new REPL commands much more pleasant.