Expected behavior: Behavior of replacement should be independent of whether the editor is open multiple times
Actual behavior: If the file is open once, then I get α (good), but if the file is open twice, then I get α (bad).
Versions
[Version of vscode-lean4 (Hover over 'lean4' in the 'Extensions' menu)] 0.0.166, but the first version with this problem is 0.0.161.
[Output of lean --version in the folder that the issue occured in] Lean (version 4.7.0, x86_64-unknown-linux-gnu, commit 6fce8f7d5cd1, Release)
[OS version] Linux markus-z16 6.9.4-200.fc40.x86_64 #1 SMP PREEMPT_DYNAMIC Wed Jun 12 13:33:34 UTC 2024 x86_64 GNU/Linux
Description
If the same file is open in multiple editors, then typing
\ainsertsαinstead ofα.Steps to Reproduce
Expected behavior: Behavior of replacement should be independent of whether the editor is open multiple times
Actual behavior: If the file is open once, then I get
α(good), but if the file is open twice, then I getα(bad).Versions
[Version of vscode-lean4 (Hover over 'lean4' in the 'Extensions' menu)] 0.0.166, but the first version with this problem is 0.0.161. [Output of
lean --versionin the folder that the issue occured in] Lean (version 4.7.0, x86_64-unknown-linux-gnu, commit 6fce8f7d5cd1, Release) [OS version] Linux markus-z16 6.9.4-200.fc40.x86_64 #1 SMP PREEMPT_DYNAMIC Wed Jun 12 13:33:34 UTC 2024 x86_64 GNU/LinuxImpact
Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.