Rename symbol dialog does not do unicode input translation

[kuruczgy]

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

1. Press F2 over an identifier.
2. 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.

[mhuisi]

The rename dialog in VS Code is unfortunately not configurable and not extendable, so we can't provide Unicode input within it.