You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Looking through the documentation, it seems we MUST have a token to start each line in a multi line comment.
Three-piece comments must
have a middle string because otherwise Vim can't recognize the middle lines.
Wtf vim.
I don't know the best solution here, but removing multilines entirely would work for me.
On February 20, 2024 2:56:42 a.m. PST, Noon van der Silk ***@***.***> wrote:
Thanks for this lovely plugin! I'm beyond excited to be able to agda in vim :)
One thing I noticed is that if I begin a multi-line comment block, then I press `Enter` to go to a newline, I get single-line comment prefixes inserted:
![image](https://github.com/isovector/cornelis/assets/129525/55c355dd-8f60-4c47-aaed-d12eef3af50b)
This was created by typing:
```Hello<cr><cr><cr><cr><cr>
```
@googleson78 suggests that perhaps a fix could be to not tag `{- -}` as comments; i.e. remove this:
```
setlocal comments=sfl:{-,mb1:--,ex:-},:--
```
But perhaps there is another alternative!
Thanks :)
--
Reply to this email directly or view it on GitHub:
#138
You are receiving this because you are subscribed to this thread.
Message ID: ***@***.***>
Thanks for this lovely plugin! I'm beyond excited to be able to agda in vim :)
One thing I noticed is that if I begin a multi-line comment block, then I press
Enter
to go to a newline, I get single-line comment prefixes inserted:This was created by typing:
@googleson78 suggests that perhaps a fix could be to not tag
{- -}
as comments; i.e. remove this:But perhaps there is another alternative!
Thanks :)
The text was updated successfully, but these errors were encountered: