VSCode: apostrophe is part of a word

Stream: general

[Kenny Lau]

In mathlib naming convention, if two lemmas have the same name, the later one is to be appended an apostrophe. For example:

nat.add_sub_cancel : ∀ (n m : ℕ), n + m - m = n

nat.add_sub_cancel' : ∀ {n m : ℕ}, m ≤ n → m + (n - m) = n

However, VSCode doesn't think the apostrophe is part of the word, in the sense that double-clicking to select a word doesn't include the apostrophe, etc. Can we change this? Thanks.

[Shing Tak Lam]

Putting this in your settings (JSON) should do?

    "[lean]": {
        "editor.wordSeparators": "`~!@#$%^&*()-=+[{]}\\|;:\",.<>/?"
    },

[Kenny Lau]

actually there is a caveat to this: 'a' is a char

[Shing Tak Lam]

Another caveat I guess? a'b'c'd'e is a valid identifier. ' is a valid part of an identifier except as the first character. So you need something which can handle asymmetric rules.

def a'b'c'd'e := 1

#print a'b'c'd'e

(btw this breaks VSCode syntax highlighting)

[Bryan Gin-ge Chen]

The syntax highlighting is probably fixable.

Given the caveats, I don't know if there's a way to handle apostrophes properly in the current state of VS Code.

As a side note, my editor.wordSeparators for Lean contains some more funny brackets:

"[lean]": {
        "editor.rulers" : [100],
        "editor.wordSeparators" : "`~!@#$%^&*()-=+[{]}\\|;:'\",.<>/?⟨⟩⦃⦄‹›⟦⟧⟮⟯",
     },

(Remove the apostrophe if you don't want VS Code to break up words at apostrophes, keep it if you do.)

[Scott Morrison]

Given nearly everyone is using VSCode, can we just include a settings file with a bunch of this useful stuff in the mathlib repo?

[Scott Morrison]

I am too incompetent / lazy to maintain local settings. :-)

[Patrick Massot]

Do you mean something like https://github.com/leanprover-community/mathlib/blob/master/.vscode/settings.json?

[Scott Morrison]

Oh. :-)

[Scott Morrison]

Can we put more things there, like turning off "auto-complete on enter" which is quite painful?

[Patrick Massot]

I vote yes since I have this locally.

[Jalex Stark]

vague issue raised at #3186, the key phrase is "can anyone that has nice local settings propose them in a PR?"