Source worth looking at for Lsp internals

Stream: lean4

[nrs]

I'd like to figure out the specifics about how the Lean server handles requests and notifications from the editor. In particular, I'd like to understand the details about where the source specifies how the server reads and writes to stdio or unix sockets, and the sequence of events that trigger a response either on cursor location change or on file modification. Any suggestions? Currently browsing around src/Lean/Server semi-randomly to get a high-level overview

[David Renshaw]

Not sure about other editors, but in emacs you can turn on logging of lsp requests with (setq lsp-log-io t)

[David Renshaw]

then you can watch the *lsp-log* buffer

[David Renshaw]

(though maybe that's higher-level than what you are looking for)

[nrs]

Am on nvim but there's an analogue to that command, will make use of that, thanks for the suggestion!

[nrs]

in case someone else finds this useful: src/Lean/Server/Readme.md is a good intro to the server's structure

[Max Nowak 🐉]

You could have a look at the code for semantic token handling.

[Max Nowak 🐉]

I should maybe some day push for my semantic highlighting changes to get merged :P.

[nrs]

Nice I had skipped this, thank you!
edit: also worth looking: the section in Sebastian Ullrich's thesis chapter 3 about the user interface, and the work by Joscha A. Mennicken cited there