Suggestion for web editor

Stream: new members

[Matt Diamond]

Is there a way to change the web editor so that it doesn't show autocomplete suggestions if you're trying to type a symbol shortcut (e.g. \l to get the left arrow)? It makes it more difficult to use symbol shortcuts because hitting space or tab will often select the autocomplete suggestion rather than entering the symbol.

[Matt Diamond]

Just wanted to bump this in case anyone has a suggestion, as this continues to be a pain point whenever I'm using the web editor. It would be nice if the web editor temporarily disabled autocomplete while you're inputting a symbol shortcut (i.e. when you type \ and the subsequent text is underlined).

[Jakub Nowak]

Which web editor do you mean? I don't have this problem on https://live.lean-lang.org/. I typed the following, and it doesn't complete l for me.

example := \l

And it does complete if I type example := l

[Matt Diamond]

it looks like autocomplete draws from existing text... try this:

/-- lalala -/
example :=

[Jakub Nowak]

Ah, I see. I've never noticed this being a problem. For me it doesn't complete after clicking Space, nor Enter. Only with Tab.

[Matt Diamond]

that's a good point, I should just stick to using the space bar instead of tab

[Jakub Nowak]

It would be nice to add completions for \, so that it shows all abbreviations. Implementing this would also solve your problem.