Nudge mobile users to switch off auto-typing features

[TentativeConvert]

Typing on a mobile phone is awkward. For me, the display is updated only on very second letter, and more generally the input is often partially hidden. This equally effects the "command line"/typewriter and editor mode. The behaviour is a bit better than for the lean3 web editor, which on my phone is completely unusable with the standard keyboard, but still unsatisfactory.

I thought initially that this was just some idiosyncatic behaviour of my specific phone/browser/etc., but after a tiny bit of research it now seems more plausible to me that this is simply the general state of affairs for the Monaco editor, which we employ (right?). The fourth sentence on the official webpage reads:

The Monaco editor is not supported in mobile browsers or mobile web frameworks.

While demand for mobile support appears to be high within Monaco's user base, not even a fallback to a simple textarea has been implemented to date within Monaco.

On my phone (Samsung, Android OS), the problem can be mitigated by using a different keyboard in place of the default keyboard (eg. BeHe). Maybe we should make users aware of this.

[joneugster]

I cannot reproduce this with my phone and the version online currently. (Android 12, Motorola, Opera)

Only thing off I see is that the scrolling isnt always perfect. Typing works like a charm.

Need to experiment with different phones (and browsers?)

[TentativeConvert]

Problems with typing, scolling perfect:

• Android 12/One UI 4 + Samsung phone + Firefox (+ default Samsung keyboard)
• Android 12/One UI 4 + Samsung phone + Chrome (+ default Samsung keyboard)

Typing ok, scrolling buggy (and menu bar not fixed):

• iOS 16.6 + iPhone 13 + Safari (+ default keyboard)
• iOS 16.6 + iPhone 13 + Chrome (+ default keyboard)

[abentkamp]

Yes, I have problems with typing, too (Chrome on Xiaomi Mi Note 10, Android 11, MIUI 13)

[abentkamp]

We could replace the input field in typewriter mode by a regular text input field. We would have to reimplement unicode input then, but I think that would be ok. Or do we want autocomplete or something else that's only available in the editor?

[joneugster]

I think we disabled autocomplete because it would also suggest Lean stuff that's irrelevant to the player, and I don't think it has been missed too much. I think a normal text-input would work

[TentativeConvert]

I would certainly be happy with a simple text-input. But I'm not sure it's worth investing into such a workaround, given that the mobile support of the Monaco editor does appear to improve over time (despite all public announcements to the contrary.) A pointer to non-default mobile keyboards might be enough.

[TentativeConvert]

And what if in some distant future version we want to try to implement autocomplete for the subset of commands/lemmas/etc. available to the player at that point in the game? Such a feature would surely be handy, especially on a mobile. Any work invested in a workaround now would then have to be undone.

[TentativeConvert]

Actually, the solution could be even simpler. Using the new dark mode of the Lean web editor, I got suspicious that the problems I experienced might be caused by some fancy autocompletion-etc features of the Samsung keyboard.

This is what typing "abc" looks like in dark mode with the Samsung keyboard, with its default settings:

The text only turns the correct colour (and becomes fully visible) once I hit whitespace:

And voila – switching off something called "Texterkennung" in the keyboard settings solved the issue for me.

[joneugster]

@TentativeConvert what's the status of this issue now? We concluded that it's a problem that Monaco is incompatible with Autocorrect, which seems beyond our control, doesn't it?

Should we close this issue by adding a comment to the documentation or should we do anything?

[TentativeConvert]

I think the best solution would be a short “warning message” to mobile users.

[joneugster]

Lean published a way to use the abbrevations in any input field: https://www.npmjs.com/package/@leanprover/unicode-input-component?activeTab=readme

This means in Typewriter mode this problem should not exist anymore once we completely use this package, started a test on dev.