In Idris2, the file will not load at all while it contains errors. This means that none of the commands will work.
I haven't gotten an answer yet as to whether it's a bug or intended behaviour, but in the meantime, this extension should notify the user that their command won't work until the errors are fixed (at least the error highlighting is working now).
Currently, the load file function doesn't look at errors, because the only way for it to fail in Idris 1 was if the file didn't exist.
In Idris2, the file will not load at all while it contains errors. This means that none of the commands will work.
I haven't gotten an answer yet as to whether it's a bug or intended behaviour, but in the meantime, this extension should notify the user that their command won't work until the errors are fixed (at least the error highlighting is working now).
Currently, the load file function doesn't look at errors, because the only way for it to fail in Idris 1 was if the file didn't exist.