-
Notifications
You must be signed in to change notification settings - Fork 49
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Embedding other LSP servers for code examples in a tex document #824
Comments
@alexkeizer
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.
It requires some work (the lifetime of the LSP servers need to be managed by
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. |
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). |
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
or
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?
The text was updated successfully, but these errors were encountered: