[bug] The selectionRange request only returns the range of one position of the sent positions

[driverag22]

Describe the bug When using the textDocument/selectionRange request, to which I pass a TextDocumentIdentifier and an array of positions, instead of getting back an array of ranges for each of the positions I get back an array with a single range for one of the positions.

To Reproduce The code I used that leads to this error can be found below (in a screenshot as well as simply copied over), together with the output. Steps to reproduce the behavior:

1. Make a positions array with >1 positions in a valid document.
2. Make a SelectionRangeParams object with the respective TextDocumentIdentifier and the positions array.
3. Pass the params to a selectionRange request.
4. The return array should be length 1 instead of the length of the original positions array.

Expected behavior After sending the request I expect the returned array of ranges to contain one range per position sent. In other words, the length of the return array should be equal to the length of the position array passed in the request.

Screenshots The output we get and relevant piece of code:

Code:

const document = this.activeDocument;
if (!document) return;
const positions: Position[] = diagnostics.map(d => d.range.start);
const params: SelectionRangeParams = {
     TextDocumentIdentifier.create(document.uri.toString()),
     positions: positions
};
try {
     const ranges = await this.sendRequest(selectionRangeRequest, params);
     if (!ranges) return;
     console.log(ranges);
     console.log(positions);
     console.log(diagnostics);
} catch (reason) {
     console.log(reason);
     return;
}

Desktop (please complete the following information):

• Arch linux
• coq-lsp version: 0.1.8+8.17
• VS Code: 1.86.1

Additional context This occurred while working on waterproof-vscode, which is a vscode extension and coq editor that relies on coq-lsp. The error should occur on the normal coq-lsp plugin directly. From a talk with Emilio, the problem seems to be that the code is currently lazy and only checks the first position instead of iterating over the array.

[ejgallego]

Hi @driverag22 , indeed this is a known todo, sorry for that. I actually looked into fixing it but it turns out that this particular LSP request is very specific so I'd have to add some custom code for it.

Question, when is the moment you usually call selectionRange ? When the document has ended checking?

[driverag22]

Question, when is the moment you usually call selectionRange ? When the document has ended checking?

Hello @ejgallego, we indeed usually call the request when the document has ended checking.

We have a setting where the user can choose whether to display detailed errors, i.e., the squiggly underline only shows at the characters related to the error, or line-long errors where the underline is extended to the whole line.

[ejgallego]

Question, when is the moment you usually call selectionRange ? When the document has ended checking? Hello @ejgallego, we indeed usually call the request when the document has ended checking.

Good, then this call should work fine; as of now, the request will wait on the highest point that was requested to be ready.

Note that I didn't add a test case, maybe that's something good for us to do.

We have a setting where the user can choose whether to display detailed errors, i.e., the squiggly underline only shows at the characters related to the error, or line-long errors where the underline is extended to the whole line.

Actually for this use case, I think you would be much better served by coq-lsp including that information in the diagnostic itself. So we could add to the extra field for errors a sentenceRange parameter that contains precisely this information. Then you could just choose at the time you are displaying the diags without a further callback.

What do you think?

[driverag22]

So we could add to the extra field for errors a sentenceRange parameter that contains precisely this information. Then you could just choose at the time you are displaying the diags without a further callback.

What do you think?

That would be lovely and would indeed probably fit better for our use case and make the editor much more responsive.

[ejgallego]

Done in #670 , it needs testing tho, but seems to work here.

[driverag22]

Thank you, I will let you know how it goes in the coming days.