Bug in lean web editor

Stream: lean4

[Shreyas Srinivas]

Since at least the last two days the following happens. When I enter \N <Tab>, first \N turns to \n which then becomes ¬. When I enter \N <Space>, I get ℕ. This is very confusing since I more often use tab for completions.

[Shreyas Srinivas]

Hitting \N <Tab> should produce ℕ normally

[Jovan Gerbscheid]

I just tried it, and for me it did create ℕ. However, I usually use Tab to avoid creating space after the symbol, and in this case it inserted 2 spaces after ℕ instead of 0 :face_with_raised_eyebrow:

[Shreyas Srinivas]

Tab is just supposed to be for completion..

[Shreyas Srinivas]

Also, if it matters, I am on firefox

[Jovan Gerbscheid]

I'm on Edge

[Jovan Gerbscheid]

I tried it on Firefox, and got the same result

[Damiano Testa]

I get the same behaviour as Shreyas: \N <Tab> converts to \n and a second <Tab> converts to ¬ (including the two spaces). I'm on Firefox (on Linux).

[Jovan Gerbscheid]

(I'm on windows)

[Jovan Gerbscheid]

The 2 spaces can also be 1 space. It always goes to an odd position from the start of the line.

[Jon Eugster]

Might well be, that part hasn't been updated since about Feb 2023. I'm on holidays for the next two weeks, but there will be a bigger update - which Alex Bentkamp worked on - soon after that.

Regardless, if you create a quick github issue it's more likely that I'll remember to test this.