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

DafnyVSCode / Dafny-VSCode

Dafny 2 for Visual Studio Code (Legacy)

MIT License

18 stars 12 forks source link

Open fmehta opened 7 years ago

fmehta commented 7 years ago

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 commented 5 years ago

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