Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Description
I tried to keep the following isolated in their own commits so we can just ditch anything folks don't like.
Whereas the CLI for the REPL currently only pays attention to one argument as an input file but quietly ignores the rest, I've made it an error to specify multiple input files:
This is further improved (described in the last section below) by using
die
instead of an uncaughtthrow
so the error doesn't look so unexpected.Whereas the REPL previously printed an error about a file loaded with
:l
in monochrome without fanfare, I've indented the error message, given it room to stand out, and written the context of the error in the standardIdrisAnn
color for error messages.Whereas on launch the REPL previously printed a subtly different error when a requested file could not be loaded than it did when using the
:l
command inside the REPL, I've aligned the two errors (and indeed refactored them to use the same code). I've also added a suggestion specifically for this startup use-case because it is common to see people intend to run e.g.idris2 --repl ...
but instead typeidris2 repl ...
which causes the REPL to attempt to load a file named "repl" -- the suggestion is that the user may have meant to writeidris2 --repl ...
so this should ease the pain of a common mistake.As mentioned above, this PR finally switches from uncaught
throw
for rendering errors from the CLI over to usingdie
so we get a less buggy looking printout. This commit also adds in a suggestion when relevant similar to the one seen within the REPL session for the above case.Should this change go in the CHANGELOG?
implementation, I have updated
CHANGELOG_NEXT.md
(and potentially alsoCONTRIBUTORS.md
).