is there an easy way to put back some old coq ide features?

[osa1]

First of all, thanks for this great work.

I want to have some old coq ide vim plugin features in coquille,

• in old plugin it was possible to send comment blocks to coq separately, but now when I send next block it consumes all comments and sends up to next definition. I don't want this.
• in old plugin, cursor was moving to last evaluated block automatically. I want to have that feature.

unfortunately I don't know enough vimscript. Is it possible to have that features with some flag or option or do I need to find relevant code and replace?

Thanks,

[trefis]

Hi!

I added an option to automatically move when sending blocks to Coq.
But while it could be done, I'm not fond of send comments between two definitions separately from the second one.
Why do you want that?

[osa1]

Thanks. Unfortunately it doesn't work:

"Sub.v" 1595L, 56905C
E189: "err.out" exists (add ! to override)
Traceback (most recent call last):
  File "<string>", line 1, in <module>
  File "/home/omer/rcbackup/.vim/bundle/coquille/autoload/coquille.py", line 165, in coq_next
    if (vim.eval('g:coquille_auto_move') == 'true'):
vim.error: invalid expression
Error detected while processing :
E121: Undefined variable: g:coquille_auto_move
E15: Invalid expression: g:coquille_auto_move
"various.txt" [readonly] 648L, 26143C

as for sending comments separately, here's my use case: I'm reading Software Foundations and it has new comment block for every one or two paragraphs and it makes reading really easier, because currently if I <F3> it sends huge amounts of text to Coq and it means it moves cursor to 1000 lines below.

While using old Coq ide plugin I was reading whole text just by doing <F3> but now I need to manually move cursor. (and still need to do <F3>)

[trefis]

Thanks. Unfortunately it doesn't work:

My bad, that is now fixed.

as for sending comments separately, here's my use case: I'm reading Software Foundations and it has new comment block for every one or two paragraphs and it makes reading really easier, because currently if I it sends huge amounts of text to Coq and it means it moves cursor to 1000 lines below.

While using old Coq ide plugin I was reading whole text just by doing but now I need to manually move cursor. (and still need to do )

Right.
I will have a look at it tomorrow then :)

[osa1]

Thanks, cursor moving thing works nicely.

[trefis]

Hi!

Sorry I didn't get back to you sooner. I had a look at this feature and as I feared, it turned out to be "a hack", i.e. coqtop doesn't support receiving just comments, you need to send them with a definition.
So to have this feature one would need to tell the user the comments have been sent while they're actually not sent, but one should remember them to send them "next time".
While that's not too hard to implement I feel like it would make the code more obscure, so I won't do it for the time being. The protocol to discuss with coqtop has changed recently on the coq repository and I want to have a look at that first; if it doesn't improve on this particular situation, I'll implement what you ask then.

[trefis]

(The close was the result of an error on my part, I push a wrong branch to github, that branch contained a commit claiming to fix this issue, but it didn't.)