search

banacorn / agda-mode-vscode

agda-mode on VS Code
https://marketplace.visualstudio.com/items?itemName=banacorn.agda-mode
MIT License
169 stars 39 forks source link

Jump to the middle of goals #100

Closed ncfavier closed 2 years ago

ncfavier commented 2 years ago

Currently the next/previous goal commands jump 3 characters after the opening curly brace, which is a problem if some space was deleted in the placeholder.

Jump to the middle of the interval instead.

Tested.

banacorn commented 2 years ago

Hi, thank you for this PR!

which is a problem if some space was deleted in the placeholder

But could you elaborate a bit more on this problem? Do you mean that when the hole has no space in it like {!!}?

ncfavier commented 2 years ago

Yes, in that case the cursor jumps after the second !

banacorn commented 2 years ago

I'm now a bit hesitant about jumping right into the middle of any hole, because I think most users are used to advancing only 3 characters when jumping to a hole. I'm thinking maybe we should only jump into the middle of a hole when it's {!!}.

ncfavier commented 2 years ago

then add a min(3, ...)

banacorn commented 2 years ago

Thank you!!