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

Do not kill LSP server process when exception occurs in doc change handler, and prevent out of range exception #2664

Merged
merged 16 commits into from
Sep 1, 2022

Conversation

keyboardDrummer
Copy link
Member

@keyboardDrummer keyboardDrummer commented Aug 31, 2022

Changes

Testing

Manual testing with VSCode

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

Copy link
Member

@MikaelMayer MikaelMayer left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Just minor updates

RELEASE_NOTES.md Outdated Show resolved Hide resolved
RELEASE_NOTES.md Show resolved Hide resolved
message = "Related location (could not read file " + fileName + ")";
}
var content = File.ReadAllText(fileName);
message = FormatRelated(content.Substring(range.StartToken.pos, rangeLength));
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I guess trading the previously optimized code for this simple but costly one is worth the fact that we don't need to deal with encodings. That's fair.

Copy link
Member Author

@keyboardDrummer keyboardDrummer Aug 31, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think all included files should be loaded into memory and available through some in memory filesystem, so then there wouldn't be any file read here. The file read here seems like it might significantly effect performance, but at least it's better than the crash.

keyboardDrummer and others added 3 commits August 31, 2022 23:08
Co-authored-by: Mikaël Mayer <MikaelMayer@users.noreply.github.com>
Co-authored-by: Mikaël Mayer <MikaelMayer@users.noreply.github.com>
RustanLeino
RustanLeino previously approved these changes Aug 31, 2022
atomb
atomb previously approved these changes Aug 31, 2022
Copy link
Member

@atomb atomb left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This looks good to me. It has the further advantage that it'll properly respect the encoding of the file (assuming that the token position and length do) rather than using byte offsets.

@keyboardDrummer keyboardDrummer enabled auto-merge (squash) September 1, 2022 12:17
@keyboardDrummer keyboardDrummer merged commit 0d7e282 into dafny-lang:master Sep 1, 2022
@keyboardDrummer keyboardDrummer deleted the textFromOtherFile branch September 1, 2022 12:51
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

Successfully merging this pull request may close these issues.

Language server crashes for the following program
5 participants