Description
When I want to rename a symbol (by pressing F2), I cannot easily input a unicode identifier, the unicode input sequences are not translated. If I try to type the sequence and press enter anyway, I get the following error:
Failed to process request 10622: Can't rename: \ph\1 is not an identifier
Context
Steps to Reproduce
- Press F2 over an identifier.
- Type
\ph\1
Expected behavior: The input is changed to φ₁
Actual behavior: The input stays exactly as typed.
Versions
[Version of vscode-lean4 (Hover over 'lean4' in the 'Extensions' menu)] v0.0.220
[Output of lean --version in the folder that the issue occured in] Lean (version 4.24.0, commit v4.24.0, Release)
[OS version] NixOS 25.05 (Warbler)
Impact
Minor annoyance. The workaround is to type the identifier in the editor somewhere else, and copy-paste it into the rename dialog
Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.
Description
When I want to rename a symbol (by pressing F2), I cannot easily input a unicode identifier, the unicode input sequences are not translated. If I try to type the sequence and press enter anyway, I get the following error:
Context
Steps to Reproduce
\ph\1Expected behavior: The input is changed to
φ₁Actual behavior: The input stays exactly as typed.
Versions
[Version of vscode-lean4 (Hover over 'lean4' in the 'Extensions' menu)] v0.0.220
[Output of
lean --versionin the folder that the issue occured in] Lean (version 4.24.0, commit v4.24.0, Release)[OS version] NixOS 25.05 (Warbler)
Impact
Minor annoyance. The workaround is to type the identifier in the editor somewhere else, and copy-paste it into the rename dialog
Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.