Unsaved buffers in vscode

Stream: lean4

[Eric Wieser]

In lean 3, it was possibly to open a lean 4 project, then create an unsaved buffer (new file) and write lean code in it. In lean 4, the file doesn't seem to compile properly until given a filename. Is this a consequence of a deliberate design change, or an unimplemented feature?

[Max Nowak 🐉]

At least in VSCode, I can create a new unsaved file and Lean 4 will work in it, including infoview.