Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Dafny project file improvements #475

Merged
merged 4 commits into from
May 9, 2024
Merged

Dafny project file improvements #475

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
76e8f51
Treat Dafny project files as a different VSCode language, so they do …
keyboardDrummer May 7, 2024
cb70fa0
Add syntaxes
keyboardDrummer May 7, 2024
854dbe4
Remove unnecessary things
keyboardDrummer May 8, 2024
9f4eac4
Remove garbage
keyboardDrummer May 8, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
0 language-configuration.json → dafny-language-configuration.json
View file
Open in desktop
File renamed without changes.
9 changes: 5 additions & 4 deletions package.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,9 @@
"bugs": {
"url": "https://github.com/dafny-lang/ide-vscode/issues"
},
"activationEvents": [
"onLanguage:toml"
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

Copy link
Member Author

@keyboardDrummer keyboardDrummer May 9, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ok, I can live with that for now.

],
"qna": false,
"license": "MIT",
"galleryBanner": {
Expand Down Expand Up @@ -123,10 +126,9 @@
],
"extensions": [
".dfy",
".dfyi",
"dfyconfig.toml"
".dfyi"
],
"configuration": "./language-configuration.json"
"configuration": "./dafny-language-configuration.json"
}
],
"grammars": [
Expand Down Expand Up @@ -309,7 +311,6 @@
}
]
},
"activationEvents": [],
"scripts": {
"vscode:prepublish": "npm run package",
"compile": "webpack",
Expand Down
6 changes: 5 additions & 1 deletion src/language/dafnyLanguageClient.ts
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -152,7 +152,11 @@ export class DafnyLanguageClient extends LanguageClient {
};
const diagnosticsListeners: ((uri: Uri, diagnostics: Diagnostic[]) => void)[] = [];
const clientOptions: LanguageClientOptions = {
documentSelector: [ DafnyDocumentFilter ],
documentSelector: [ DafnyDocumentFilter, {
scheme: 'file',
pattern: '**/*dfyconfig.toml'
}
],
diagnosticCollectionName: LanguageServerId,
middleware: {
handleDiagnostics: (uri: Uri, diagnostics: Diagnostic[], next: HandleDiagnosticsSignature) => {
Expand Down
Loading