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: https://github.com/DafnyVSCode/Dafny-VSCode/blob/b8b75aff327cad0884d2a19fa844b7702e1a5f4f/server/src/server.ts#L34