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

Cannot type unicode superscript in `∧-zeroˡ` #145

Closed uhbif19 closed 1 year ago

uhbif19 commented 1 year ago

Lookup says that ^l will give me this superscript symbol. But once I type \^r I get some box superscript symbol.

This is copypasted result for typing this after x: ⃗x⃗.

Same with r.

L-TChen commented 1 year ago

Hi, you need to switch to a font that covers more Unicode characters, if you only see a little box.

There are 4 possible characters for ^l and ^r (see screenshots below),

Screenshot 2023-07-25 at 14 58 23Screenshot 2023-07-25 at 14 58 06

The first choice of \^r and \^l is indeed a combing character, so this is the intended behaviour.

uhbif19 commented 1 year ago

Thanks, missed that.

Hi, you need to switch to a font that covers more Unicode characters, if you only see a little box.

Copying manually seems fine. Seems like box is only for combing cases, probably that is how it supposed to work or bug in FiraCode.