improvement for vim navigation

[qcfu-bu]

Using vscoq's interpret to point command, the current line of proof that the cursor is on is not interpreted. This causes a bit of inconvenience when using with the vscode vim extension. Basically using vim, it is impossible to place the cursor in such a way that the interpret to point command interprets the current line. This is inconsistent with the behavior of proof general in emacs where the interpret to point includes the line of proof that the cursor is currently on.

[gares]

IIRC PG has an option to change the meaning of "here". But I see your point.
I don't know if the best action is to add such an option, or to add another command, i.e. "interpret to next point".

[rtetley]

I honestly don't have an opinion. Is it important to keep both options ?

[TheoWinterhalter]

One thing I'm wondering is what would happen if your cursor is in between to sentences, which one would be interpreted as "the point"?

Using a pipe for the cursor:

tac1. | tac2.

Here I would expect "Interpret to point" to only process up to and including tac1 but I would be very surprised if it were to include tac2 as well.

ta|c1. tac2.

There I would be ok with it being the same, ie interpreting tac1 too.

[rtetley]

That's a good point. Unfortunately I think currently those spaces would be interpreted as being part of the tac2 command. I have to check particulars.

[qcfu-bu]

One thing I'm wondering is what would happen if your cursor is in between to sentences, which one would be interpreted as "the point"?

Using a pipe for the cursor:

tac1. | tac2.

Here I would expect "Interpret to point" to only process up to and including tac1 but I would be very surprised if it were to include tac2 as well.

ta|c1. tac2.

There I would be ok with it being the same, ie interpreting tac1 too.

When I try interpret to point in emacs, it will only include tac1. and not tac2.