cursor position is off when some unicode characters are used

[leodemoura]

I noticed the problem with two characters \and and \forall. For example, try to input

theorem tst : ∀a b: Prop, a ∧ b → a ∧ b:= 

The cursor position is so off that it is not even funny.

[leodemoura]

http://stackoverflow.com/questions/20931029/ace-editor-monospace-fonts-issues-with-cursor-spacing

[leodemoura]

https://github.com/ajaxorg/ace/issues/1666

[soonhokong]

@leodemoura, I think I fixed the problem. Could you test http://leanprover.com ? I've tested it on (Windows, OSX, Ubuntu) x (IE, Chrome, Firefox, Safari) combinations and I couldn't find a problem.

[leodemoura]

I tried the following

open num eq.ops
check ∀x y, x ∧ y → y ∨ x
check λ (x y : num) (H₁ : x = y) (H₂ : y = x), (H₁ ⬝ H₂)⁻¹⁻¹

• Windows 8.1 + Chrome
  • cursor position is correct
  • transitivity operator is not available ⬝
• Windows 7 + Chrome
  • same behavior of Windows 8.1 + chrome
• Windows 8.1 + IE
  • \all, \or, \and work
  • cursor position is incorrect when subscript is used (we can produce them using \1 \2 ...)
  • the transitivity operator is displayed correctly
• Ubuntu 12 + Chrome
  • cursor position is incorrect when we use \tr (transitivity operator)
• Ubuntu 14 + Chrome
  • cursor position is incorrect (BTW, I believe it was working before)
• Ubuntu 14 + Firefox
  • cursor position is incorrect

[soonhokong]

I see. I will add more fonts on the list. Thanks for testing it.

[soonhokong]

I think the transitivity operator (⬝) is a monster. I have a problem with OSX.

Ubuntu 14 + Chrome

• cursor position is incorrect (BTW, I believe it was working before)

Nope. It has the same problem with old configuration.

[soonhokong]

The problem is solved by using GNU Free Mono font. I used http://www.fontsquirrel.com/tools/webfont-generator to generate the web fonts of GNU Free Mono. This ensures the same user experience across platforms.