search

ashinkarov / nvim-agda

Agda interaction pluging for neovim
36 stars 5 forks source link

`commentstring` missing #6

Open siers opened 2 years ago

siers commented 2 years ago

Hi!

Plugins like https://github.com/tpope/vim-commentary check the commentstring to get the formatting required to comment out lines. The other plugin I used had it https://github.com/derekelkins/agda-vim/blob/master/ftplugin/agda.vim#L64 and it seems like this is a simple enough change.

Maybe it's worth adding it?

siers commented 2 years ago

It looks like it also sets setlocal comments=sfl:{-,mb1:--,ex:-},:--, but I'm not sure what effect that has.

ashinkarov commented 2 years ago

This sounds to me like a user-specific option. Is there a reason why this needs to be hardcoded in the plugin? I would assume that users may specify this variable for .agda files via autocommand.

siers commented 2 years ago

It seems like nvim-agda is a general agda plugin, because it not only implements agda-mode's (actually I don't know what exactly agda-mode implements, since I'm not an emacs user) communication with agda backend, but also already provides language related editor niceties in the form of unicode inputs.

So to me it would make sense that some integration with the vim plugin ecosystem would also find its place in this repo, especially since declaring commenting syntax is something that each user would have to repeat exactly, if declaring this string is up to the user. I do believe many language plugins (just like agda-vim) declare this string, but this is probably believable, so I won't go search for examples.

ashinkarov commented 2 years ago

One problem with such nicities is that they essentially introduce a dependency (to another plugin). Just imagine that somebody wants to use a different plugin where these variables have a completely different (undesirable) meaning. How do you turn it off, in case it is hardcoded? Plugins are compositional when they expose as little as possible dependencies. I am happy to consider extensions when users cannot achieve a certain functionality. However, this doesn't seem to be the case here.

siers commented 2 years ago

It should be redefinable in user's own configuration as they usually can make it run last.

I do think in this case the benefits are clear and the problems are likely to be so rare that it's not worth considering them unless they do, in fact, arise. :) The lines in question are still present in agda-vim, after all.

Though I understand that this request may not be clearly motivated for those users not used to commentary.vim or similar. Maybe other users eventually will chime in and offer their point of view. :)

jliptrap commented 2 years ago

commentstring doesn't introduce a dependency.