Finish implementation of "document highlight" request

[Kha]

We already have a handler for textDocument/documentHighlight, but it only highlights the corresponding do of a return, which is a bit awkward as mentioned in leanprover/vscode-lean4#103 (comment). After #835, we have all the information we need to implement highlighting of identifiers as well.

[Kha]

After #835, we have all the information we need to implement highlighting of identifiers as well.

We currently send this data to the watchdog without storing it in the file worker, but I think it's better to keep the request handler in the worker (the do part certainly should stay there).

[gebner]

We currently send this data to the watchdog without storing it in the file worker, but I think it's better to keep the request handler in the worker (the do part certainly should stay there).

It would also be great if the references could already be shown before the whole file has been compiled (i.e., only show the references in the already finished part). This also requires the code to stay in the worker.

[Kha]

That would be great for many many requests, but I don't think there's anything we can do other than to wait for editors to finally implement support for partial results. To be honest, I kind of hoped that VS Code would before people started to write complicated files in Lean 4. Does Neovim?

[Kha]

I don't think there's anything we can do other than to wait for editors to finally implement support for partial results

For reference

VS Code: microsoft/vscode#105870
Emacs: emacs-lsp/lsp-mode#1117

[gebner]

That would be great for many many requests, but I don't think there's anything we can do other than to wait for editors to finally implement support for partial results. To be honest, I kind of hoped that VS Code would before people started to write complicated files in Lean 4. Does Neovim?

Not that I know of. I couldn't even find an issue in the bug tracker.

For "find references" etc. result streaming is really useful, since you do the request once and expect results outside of the currently shown part of the file. But for document highlights I think sending just the current state should be okay; the request is repeated every time you move the cursor and the results are primarily shown in the currently visible text. It's certainly more useful to have some results immediately than to have the complete results a minute or two later. If we wait for the whole file, then you'll never see the highlights in normal usage.

[Kha]

Right, that should be acceptable