Nonsense emoji showing in UI

[bearomorphism]

Description

Browser may incorrectly render emojis in game UI.

I'm using latest Brave browser on MacOS.

Screenshots

The HTML element looks like

<div><strong class="goal-hyp"><span class="mr1 goal-inaccessible "><span class=""><span class="highlightable ">h3✝</span></span></span></strong>:&nbsp;<span class="font-code"><span><span class="highlightable "><span class="highlightable "><span class="font-code"><span><span class="highlightable "><span class="highlightable "><span class="font-code">x</span></span></span></span> ∈ <span><span class="highlightable "><span class="highlightable "><span class="font-code">A</span></span></span></span></span></span></span></span></span></div>

[joneugster]

yep, that's because the unicode char used there is missing the text-variant selector (U+FE0E or something). I think this comes from Lean itself and I've once tried to fix this accross core & mathlib, but wasn't successful. We might be able to do some post-processing on lean4game side, or maybe just specify a proper font in the infoview.

Another solution would be that the STG4-game (which this is, I think?) adds the right leanOption to enable "tactics being unhygienic".

[bearomorphism]

Thanks