Case splitting holes after a new line are mishandled

banacorn / agda-mode-vscode

agda-mode on VS Code

https://marketplace.visualstudio.com/items?itemName=banacorn.agda-mode

MIT License

167 stars 38 forks source link

Case splitting holes after a new line are mishandled #164

Closed fredrik-bakke closed 1 year ago

fredrik-bakke commented 1 year ago

Given the following set-up:

If you attempt to case split using C-c C-c, the following is given back:

which is clearly not what you want.

jespercockx commented 1 year ago

This issue is already known in the main Agda repository: https://github.com/agda/agda/issues/1146. Since it's also present in the Emacs mode, I don't think this can be fixed easily on the VS Code side.

fredrik-bakke commented 1 year ago

Thanks, and sorry for the confusion. Is something similar also true for #158 and #159?

fredrik-bakke commented 1 year ago

Perhaps also #157?