VS code extension priority

Stream: general

[Thomas Murrills]

When I make a new file without naming it, VS code prefers to interpret it as Haskell or Python. Sometimes I like using new unsaved files for scratch work, and I just don't want the extra step of clicking "lean4" from the extension-chooser dropdown. :)

Is there a way to get VS code to interpret a file starting with import as a Lean file by default?

[Thomas Murrills]

Ah, I found one way to do it: in Settings, set Files > Default Language to lean4. (Maybe tying this setting to a workspace or profile(?) would be better if actively coding in other languages.)

[Thomas Murrills]

I'm a bit surprised that VS code's history-based language detection model (which I have enabled) consistently gets it wrong, seeing as the entire workspace and history is lean files, with no python or Haskell...