banacorn / agda-mode-vscode

agda-mode on VS Code
https://marketplace.visualstudio.com/items?itemName=banacorn.agda-mode
MIT License
167 stars 38 forks source link

`C-c` `C-r` results in wrong character when applied to character outside of BMP #173

Closed choukh closed 8 months ago

choukh commented 9 months ago

https://github.com/banacorn/agda-mode-vscode/assets/19528659/86e510e5-e182-44e5-b9af-26fbf2d3332c

banacorn commented 8 months ago

Sorry but can you offer the file for reproducing this?

choukh commented 8 months ago

: {A : Set} → A → A = λ 𝒶 → {! !} -- paste 𝒶 in the hole and refine to reproduce the bug

banacorn commented 8 months ago

Issue reproduced!