Dafny project file improvements #475
Conversation
…not get incorrect syntax highlighting
| @@ -11,6 +11,9 @@ | |||
| "bugs": { | |||
| "url": "https://github.com/dafny-lang/ide-vscode/issues" | |||
| }, | |||
| "activationEvents": [ | |||
| "onLanguage:toml" | |||
There was a problem hiding this comment.
Isn't that a bit too broad? toml is not Dafny specific. This means that the Dafny extension will start even if a toml file is run that isn't a dfyconfig. Could you please create an empty .toml file and verify that it won't crash the language server somehow?
There was a problem hiding this comment.
It is too broad. I would have preferred to set the extension to activate only when the path pattern **/*dfyconfig.toml is opened, but VSCode does not support that.
However, activating too early can not lead to bugs. Which files VSCode sends to the language server is controlled in a different location, and there the filter is more specific. Activating too early does hurt VSCode performance since the extension will run startup code even when you're just working with "*.toml" files that are unrelated to Dafny.
If I leave out this activation event, then if you open a dfyconfig.toml without opening any .dfy file, the extension does not activate and you do not get diagnostics for the Dafny project you opened. This is only a slight inconvenience, but starting the extension even when you're not doing anything with Dafny is also only slightly inconvenient.
There was a problem hiding this comment.
Ok, I can live with that for now.
| @@ -11,6 +11,9 @@ | |||
| "bugs": { | |||
| "url": "https://github.com/dafny-lang/ide-vscode/issues" | |||
| }, | |||
| "activationEvents": [ | |||
| "onLanguage:toml" | |||
There was a problem hiding this comment.
Ok, I can live with that for now.
Changes
.tomlfile is opened, such as adfyconfig.tomldfyconfig.tomlTesting
dfyconfig.tomlwill already trigger the extension and provide diagnostics.dfyconfig.tomlfile causes diagnostics to be updateddfyconfig.tomlfiles works correctly.