Keep VS Code from replacing escape sequence?

Stream: lean4

[Kyle Miller]

In the following, if you insert \" between the single quotes '', navigate to the blank line, and press the tab key, then the \" gets replaced with Ä.

def is_dquote (c : Char) : Bool :=
  if c == '' then

  else
    false

I guess if, rather than inserting \", you type \, tab, ", then this cancels \ being active. Is there a way to cancel it after typing \"? The escape key doesn't seem to do so. (Is there a way to prevent it from spookily replacing \" from a distance?)

(This is not real code, just a demonstration.)

[František Silváši]

It makes me want to strangle baby seals when my newline "\n" is replaced with a unicode negation.

[Henrik Böving]

In Emacs if you double type a \ it will ignore the unicode stuff, maybe it has been implemeted like this in vscode as well?

[Patrick Massot]

Did you follow the suggestion at https://github.com/leanprover/vscode-lean/#input--editing-settings?

[Patrick Massot]

Note that you can also use another input leader (other than \).

[Arthur Paulino]

Patrick Massot said:

Note that you can also use another input leader (other than \).

IIRC I saw in a video that you use ,. I think that's a smart move and I'm going to copy it :eyes:

[František Silváši]

Oh this is brilliant advice. I'll use a different leading character indeed. Thanks <3.

[Eric Wieser]

I think this would also be resolved by adding a Unicode completion that sends \" to itself

[Eric Wieser]

Same for \n

[Eric Wieser]

The "shortest matching prefix" behavior comes at the expense of having some bad prefixes we need to override

[Eric Wieser]

Maybe that would interfere with \"a though