Embedding other LSP servers for code examples in a tex document

[alexkeizer]

I am currently working on a .tex document featuring a lot of code snippets, and I am looking for a way to get easy feedback on the (syntactic) correctness of those snippets, literate programming style.

Right now, I am using a script that extracts all (Lean) code in

\begin{leancode}
  -- code goes here
\end{leancode}

or

\begin{leanhidden}

\end{leanhidden}

environments (the latter is for code that shouldn't show up in the pdf output) to a separate file, that I can then run through a Lean typechecker.

This setup works, but requires switching to a different window (with the extracted code file open) to get feedback.

I'm no expert on LSP, but as I understand it, if we can have texlab detect these environments and somehow forward the relevant text to the Lean LSP server, then that would enable me to edit code snippets in my .tex file with all the convenience and feedback that I would get when editing in a normal .lean file.

Does this seem like a feasible way to go, and would you be open to a PR implementing this kind of embedding of other LSP servers in texlab?

[pfoerster]

@alexkeizer Thanks for the suggestion!

I'm no expert on LSP, but as I understand it, if we can have texlab detect these environments and somehow forward the relevant text to the Lean LSP server

Yeah, this would definitely be possible. We could even go one step further and handle embedded BibTeX properly as well. At the moment, it is just ignored.

Does this seem like a feasible way to go

It requires some work (the lifetime of the LSP servers need to be managed by texlab and we need to generate artificial URIs for the code snippets).

and would you be open to a PR implementing this kind of embedding of other LSP servers in texlab

Sure, although I recommend waiting until #823 is merged because there a lot of internal changes in this PR and it would also be beneficial for this change as the type-checking could easily be done incrementally. For example, we do not need to send the code snippets to other LSP servers if the snippet did not change.

[alexkeizer]

In any case, I probably won't have time to actually dig into this until my current project is finished (after which my need for it will be much less). For future reference, I got the idea of embedding language servers from https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/IntellISense.20for.20Language.20Embeddings.3F, and that thread probably contains information that might be useful for a texlab version.