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

Holes spanning multiple lines are not handled #159

Open fredrik-bakke opened 1 year ago

fredrik-bakke commented 1 year ago

Holes spanning multiple lines are not highlighted:

image

And attempting to insert using C-c C-space does not work:

image
fredrik-bakke commented 1 year ago

Presumably, this is related to #158.

banacorn commented 8 months ago

Please reopen this issue if the problem still persists

fredrik-bakke commented 8 months ago

Thanks for taking the time, @banacorn. Unfortunately, unless the fix was not shipped with the most recent version of the extension, this problem persists.