Inconsistent step highlighting

[thery]

I am working withvscoq-language-server 2.2.1 and coq 8.19.2
Given the code

Locate nat.

Goal True.

If I do an execution to point to the last line.
The first line does not get an executed status while it does if I do a step by step execution.

[TheoWinterhalter]

I don't think highlighting is the issue, because such a line is indeed not evaluated unless you explicitly step through.

[rtetley]

Indeed @TheoWinterhalter is right.

[thery]

so interpret to point is not equivalent to step through?

[TheoWinterhalter]

It is skipping commands that would only print things. I guess it makes sense in terms of performance to ignore commands that do not modify the environment. Maybe there should be an opt-in to force them during "interpret to point"?

[gares]

I'm probably the guilty one, and I too find it confusing. IMO it should be enabled in the mode we call "skip proofs" (that should be named "skip proofs and queries".