Quick Help Needed: Lean4 LSP protocol extensions(?)

Stream: general

[io.shift]

I need resources on lean4 LSP extensions, and I can't seem to find any online. Unless lean4 doesn't have any additional LSP extensions on-top of the core LSP protocol?

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Yep, Lean uses a whole bunch of LSP extensions to support the infoview and widgets. There is not a whole lot of documentation, but most of the extensions are gathered in Lean.Data.Lsp.Extra.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Also docs#Lean.Lsp.DiagnosticWith.