Completion of keywords into identifiers

[Kha]

#check with

When typing this line, we get ident completion up to typing the h. Ideally we should get it even then.

[Kha]

Note: we should make sure to also provide the keyword itself as a completion option here, which is not the case yet

[nomeata]

That would probably fix #3462 as well.

[kmill]

Something that trips me up a lot is a popup on do, both in Lean and in Mathlib.

This Mathlib one might not be related, but I thought I'd mention it.

These are especially painful since the natural thing to do after typing do is to hit "enter", which activates the completions.

[kim-em]

I get bitten by the do completion regularly!

[mhuisi]

I get bitten by the do completion regularly!

Do you still see this issue after #3778?

Note that this issue is not about the popup issue that Kyle mentioned (which should have been resolved by #3778), but specifically about offering identifier completions when typing in keywords.

[kim-em]

Unfortunately yes:

[mhuisi]

Unfortunately yes:

That's a code snippet manually added by Mathlib, the language server is not involved here.

[leodemoura]

As far as I can tell this issue has been fixed. I cannot reproduce any of them using v4.8.0-rc2.
Closing soon.

[mhuisi]

As far as I can tell this issue has been fixed. I cannot reproduce any of them using v4.8.0-rc2. Closing soon.

The issue reported by Sebastian is still there (we don't report identifier completions for keywords), the other unrelated issues in the thread should have been fixed by #3778.