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

[fleche] New immediate request serving mode. #841

Merged
merged 1 commit into from
Sep 29, 2024
Merged

[fleche] New immediate request serving mode. #841

merged 1 commit into from
Sep 29, 2024

Conversation

ejgallego
Copy link
Owner

In this mode, requests are served with whatever document state we have.

This is very useful when we are not in continuous mode, and we don't have a good reference as to what to build, for example in documentSymbols (cc: #816)

The mode actually works pretty well in practice as often language requests will come after goals requests, so the info that is needed is at hand.

It could also be tried to set the build target for immediate requests to the view hint, but we should see some motivation for that.

This commit switches documentSymbols to the immediate mode, when in lazy checking mode.

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
In this mode, requests are served with whatever document state we
have.

This is very useful when we are not in continuous mode, and we
don't have a good reference as to what to build, for example in
`documentSymbols` (cc: #816)

The mode actually works pretty well in practice as often language
requests will come after goals requests, so the info that is needed is
at hand.

It could also be tried to set the build target for immediate requests
to the view hint, but we should see some motivation for that.

This commit switches `documentSymbols` to the immediate mode, when in
lazy checking mode.
@ejgallego ejgallego merged commit 2d8642d into main Sep 29, 2024
14 checks passed
@ejgallego ejgallego deleted the request_imm branch September 29, 2024 16:04
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

1 participant