Stream: jsCoq

Topic: `<` triggers special char autocomplete


view this post on Zulip Cyril Cohen (Dec 04 2021 at 11:50):

In https://coq.vercel.app for example (but also my own stuff) when I press <, it inserts a \ and pops up a menu for me to chose among special chars. Any idea why? Is this a local setup? is it codemirror? Is there an option I can switch somewhere? (FYI I deactivated company-coq just in case, but the problem persists)
(CC @Enrico Tassi, @Emilio Jesús Gallego Arias, @Shachar Itzhaky)

view this post on Zulip Cyril Cohen (Dec 04 2021 at 12:01):

excerpt from tex-input-hint.js:

List of open issues: [...]

- Review if the way we capture the '\' keypress comforms to CM
coding standards.

I'd say probably not? :laughter_tears:

view this post on Zulip Shachar Itzhaky (Dec 04 2021 at 12:23):

Huh, this does not happen to me. Also super weird! I have no idea why this should happen. What browser?

view this post on Zulip Cyril Cohen (Dec 04 2021 at 12:24):

google-chrome, french keyboard, french system layout

view this post on Zulip Shachar Itzhaky (Dec 04 2021 at 12:26):

Can you try to comment out this in tex-input-hint.js? To see if that's what's causing it.

      cm.addKeyMap({"\\": function(cm)
                    {
                      cm.replaceSelection("\\");
                      cm.execCommand("autocomplete");
                    }});

view this post on Zulip Cyril Cohen (Dec 04 2021 at 12:26):

If I switch to english layout, then both < and \ become special (while in the french layout only < is).

view this post on Zulip Cyril Cohen (Dec 04 2021 at 12:26):

Shachar Itzhaky said:

Can you try to comment out this in tex-input-hint.js? To see if that's what's causing it. [...]

Already tried, does not work.

view this post on Zulip Cyril Cohen (Dec 04 2021 at 12:27):

Wait no, it does work

view this post on Zulip Shachar Itzhaky (Dec 04 2021 at 12:27):

Cyril Cohen said:

If I switch to english layout, then both < and \ become special (while in the french layout only \ is).

Oh wow the plot thickens

view this post on Zulip Cyril Cohen (Dec 04 2021 at 12:29):

Cyril Cohen said:

Wait no, it does work

I'll go with it for now...

view this post on Zulip Shachar Itzhaky (Dec 04 2021 at 12:31):

Just to make sure, did you try the CodeMirror website https://codemirror.net (which contains a small editor widget as a demo)? When you type '<' there, it works correctly..?

view this post on Zulip Cyril Cohen (Dec 04 2021 at 12:32):

Shachar Itzhaky said:

Just to make sure, did you try the CodeMirror website https://codemirror.net (which contains a small editor widget as a demo)? When you type '<' there, it works correctly..?

Yes, it works correctly, and if I uncomment cm.addKeyMap({"\\": function(cm) it also works correctly

view this post on Zulip Cyril Cohen (Dec 04 2021 at 12:32):

(although I lose the use of special chars)

view this post on Zulip Shachar Itzhaky (Dec 04 2021 at 12:39):

do you have an AZERTY keyboard?

view this post on Zulip Shachar Itzhaky (Dec 04 2021 at 12:48):

I've found that the < in the AZERTY layout is located exactly where the \ is in certain layouts (British?), e.g. this SE question:
https://askubuntu.com/questions/444810/editing-keyboard-layout

view this post on Zulip Cyril Cohen (Dec 04 2021 at 12:52):

Shachar Itzhaky said:

do you have an AZERTY keyboard?

Yes I do

view this post on Zulip Shachar Itzhaky (Dec 04 2021 at 13:25):

Perhaps try an English (US) as your English layout? This is one of the most obscure bugs!

view this post on Zulip Shachar Itzhaky (Dec 04 2021 at 13:26):

@Emilio Jesús Gallego Arias @Bas Spitters What do your keyboards look like?

view this post on Zulip Bas Spitters (Dec 04 2021 at 13:31):

American and Danish :-)

view this post on Zulip Emilio Jesús Gallego Arias (Dec 04 2021 at 16:09):

Spanish / UK

view this post on Zulip Shachar Itzhaky (Dec 04 2021 at 16:55):

Hah :D

view this post on Zulip Shachar Itzhaky (Dec 04 2021 at 17:00):

Who's in for a fun experiment? Run this in your JS console, then switch back to the page and type \:

document.addEventListener('keydown', console.log)

view this post on Zulip Shachar Itzhaky (Dec 04 2021 at 17:00):

Let me know what key, code, and keyCode you get :laughing:

view this post on Zulip Shachar Itzhaky (Dec 04 2021 at 17:01):

I'm getting: key: '\\', code: 'Backslash', keyCode: 220

view this post on Zulip Shachar Itzhaky (Dec 04 2021 at 17:06):

Oh and repeat for <. Here's what mine gives: key: '<', code: 'Comma', keyCode: 188

view this post on Zulip Emilio Jesús Gallego Arias (Dec 04 2021 at 21:16):

KeyboardEvent {isTrusted: true, key: '\\', code: 'Backquote', location: 0, ctrlKey: false, …

view this post on Zulip Emilio Jesús Gallego Arias (Dec 04 2021 at 21:16):

Keycode 220

view this post on Zulip Emilio Jesús Gallego Arias (Dec 04 2021 at 21:16):

for <

view this post on Zulip Emilio Jesús Gallego Arias (Dec 04 2021 at 21:17):

code: "IntlBackslash" keycode "220"

view this post on Zulip Emilio Jesús Gallego Arias (Dec 04 2021 at 21:17):

ha!

view this post on Zulip Emilio Jesús Gallego Arias (Dec 04 2021 at 21:17):

same keycode!

view this post on Zulip Emilio Jesús Gallego Arias (Dec 04 2021 at 21:18):

what's going on!

view this post on Zulip Emilio Jesús Gallego Arias (Dec 04 2021 at 21:18):

This is with French Hardware, but spanish keyboard in Linux

view this post on Zulip Cyril Cohen (Dec 05 2021 at 11:35):

I'll try asap

view this post on Zulip Cyril Cohen (Dec 05 2021 at 12:07):

When I press <
key: '\', code: 'Backslash', keyCode: 220

view this post on Zulip Emilio Jesús Gallego Arias (Dec 05 2021 at 14:05):

Yeah the bug is confirmed, for some reason both keys have the same keycode

view this post on Zulip Cyril Cohen (Dec 05 2021 at 14:23):

I guess a possible workaround would be to read which character has actually been inserted...

view this post on Zulip Emilio Jesús Gallego Arias (Dec 05 2021 at 14:43):

or just code, but indeed, that needs fixing

view this post on Zulip Cyril Cohen (Dec 05 2021 at 14:54):

"or just code" ?

view this post on Zulip Cyril Cohen (Dec 05 2021 at 14:56):

Oh and if I type \ on my french keyboard it is AltGr+8:
key: "8", keyCode: 56, code: "Digit8"
:laughter_tears:

view this post on Zulip Cyril Cohen (Dec 05 2021 at 15:02):

key_backslash.png
key_lessthan.png

view this post on Zulip Cyril Cohen (Dec 05 2021 at 15:09):

on keypress, e.key looks fine though...
document.addEventListener('keypress', e => console.log("keypress: " + e.key)) gives me the right results

view this post on Zulip Shachar Itzhaky (Dec 07 2021 at 08:55):

perhaps... we are using CodeMirror's keymap, which hides the actual event binding, but perhaps there's a way to get the actual event, or hook into keypress instead of keydown, manually.


Last updated: Jan 31 2023 at 09:01 UTC