Skip to content
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

LSP Request Changes #35

Closed
enigmurl opened this issue Oct 23, 2024 · 3 comments
Closed

LSP Request Changes #35

enigmurl opened this issue Oct 23, 2024 · 3 comments

Comments

@enigmurl
Copy link
Collaborator

We should prioritize LSP requests to the currently opened file, especially on startup. Right now, there is sometimes a noticeable lag. Also, sometimes we send requests to a closed file and there's an error. We should try to gracefully handle these errors.

@onriv
Copy link
Owner

onriv commented Oct 24, 2024

@enigmurl also discussed in redhat-developer/lsp4ij#582

@onriv
Copy link
Owner

onriv commented Dec 4, 2024

We should prioritize LSP requests to the currently opened file, especially on startup. Right now, there is sometimes a noticeable lag.

This is possible in 0.1.7 with LSP4IJ 0.8.1, please give it a try.

Also note https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.E2.9C.94.20Compiling.20too.20slow
for Intellij auto saving files

@enigmurl
Copy link
Collaborator Author

enigmurl commented Dec 4, 2024

Seems fixed. Thanks for the hard work!

@enigmurl enigmurl closed this as completed Dec 4, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants