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

fix: mitigate abbreviation race conditions #389

Merged

Conversation

mhuisi
Copy link
Collaborator

@mhuisi mhuisi commented Jan 23, 2024

This PR attempts to resolve the race conditions that induce #332 and #373.

#332 was caused by a combination of waiting in the abbreviation provider to mitigate another issue and attempting to update the selection with a state that may be stale.

It has been resolved by removing the waiting call, refactoring the selection update logic to use a less stale state and only making the extension move the cursor manually when replacing $CURSOR abbreviations, relying on the builtin logic of VS Code to move it when issuing a text editor edit otherwise.
The former two adjustments only reduce the likelihood of a race condition, whereas the latter should resolve this issue entirely for all input where we are merely appending to an abbreviation: For non-$CURSOR abbreviations, we can rely on the VS Code transaction logic that is not subject to race conditions, whereas for $CURSOR abbreviations, there is a fixed place where we want to move the cursor to, and so we needn't worry about characters appended by the user in the meantime throwing off the "correct" cursor position that we want to move the cursor to. In the unlikely case that the text editor state suddenly changes before a $CURSOR abbreviation in the moment after we replaced it and before we moved the selection, the extension may still jump to an incorrect location. This edge case is impossible to fix as VS Code has no read-write transaction for edits and cursor updates.

#373 was caused by the fact that when issuing an edit to the VS Code text editor, the state of the text editor that the extension uses may be stale, thus leading to VS Code rejecting the edit.

This issue can unfortunately only be mitigated, not fixed, as VS Code provides no mechanism for read -> write transactions. To reduce the fallout, a retry logic was implemented. Should all retries fail, instead of deleting the abbreviation and issuing a noisy error, the extension keeps it around so that it can attempt replacing the abbreviation again whenever the user decides to edit the document or move the cursor. This is hopefully much more bearable than the immediate failure and error issuance that occurred before.

This PR also fixes another bug where the extension wouldn't replace abbreviations when moving the cursor, despite the code intending this.

Closes #332.
Closes #373.

@mhuisi mhuisi merged commit 3e33173 into leanprover:master Jan 24, 2024
2 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
1 participant