Closed scotek closed 3 years ago
I am very sorry that this PR has been the 'p' and 'r' in purgatory. Having started on some revision of the mode to accommodate breaking changes to the IDE protocol in Idris2, I saw that I missed the follow up to this. I've merged now. Very sorry about this.
This fix breaks Idris1 compatibility but I will fix that in a second commit. Thanks!
…or making a case expression from a hole with Idris 2. Fixes issue #512.
As the issue says, this leaves an extra newline at the end of the inserted response in Idris 1. It's still valid but slightly annoying. We may need to look at adding a setting to indicate Idris 1 vs 2 and tweak some of these functions but that needs a separate discussion.