What do you think of idris2-lsp-vscode?

[michaelmesser]

What do you think of idris2-lsp-vscode? It supports semantic highlighting of Idris source files.

[meraymond2]

It's cool. My assumption is that it will replace this extension when the language server catches up. I haven't been following the progress of the language server recently, but the last time I looked there was still quite a bit to do, I need to check on it again. Possibly the two can complement each other in the meantime.

I haven't looked at the semantic highlighting for source in a while, I remember it was a bit problematic. The IDE Protocol only works with files on disk. It's easy to do the initial highlighting but not easy to keep it updated when you start typing.

Off the top of my head I could

• highlight on load, and drop it all again once the user starts typing until they save again
• save the file on every change
• highlight on load, try to shift it along as edits are made, and re-highlight on save
• copy the source file to a temporary file, which could be saved on each edit

but I didn't like any of those options. I'm guessing the language server is keeping it in memory and re-parsing on each update.

[michaelmesser]

I won't recommend using both extensions at the same time. Unfortunately even the Idris API doesn't support working with unsaved files. The server relies on the client (VSCode) to shift the highlights as edits are made.

[meraymond2]

It supports semantic highlighting of Idris source files.

Do you mean that extension supports semantic highlighting already, or just that the Language Server does?

I'm thinking about taking another stab at this. It wasn't a priority before because the v2 ide-mode wasn't sending the semantic metadata, but it is now for most messages, so it could be worth doing.

[michaelmesser]

VSCode supports semantic tokens and so does the language server. The extension is fairly minimal and just connects VSCode to the language server. To support features not covered by the LSP spec the code would have to be added to the extension. When the client asks for semantic tokens about a document that is different than is on disk, the server sends RequestCancelled which is a bit of a hack. The server triggers a reload of all semantic tokens when a file is saved. VSCode intelligently moves the semantic tokens in between. Why not just switch to the LSP?