More informative warning in case a file, and not a workspace is opened.

[fmehta]

Hello,

Currently, a user who opens a single file, and not a workspace gets the following warning:

"Warn: Please use a workspace (File - Open Folder). Otherwise some features aren't working properly"

Please modify this warning to be more informative. E.g.:

"Warn: Open a workspace (File - Open Folder) instead of single files in order to XXX. More details can be found in XXX"

Thanks,
Farhad

[fabianhauser]

It would also be nice if, instead of the error message, a graceful feature reduction could happen.

Important Lines:

Dafny-VSCode/server/src/server.ts

Line 34 in b8b75af

workspaceRoot = params.rootPath;