From 76e8f511a2a3018424d090163d0dc72a0c74cb7c Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 7 May 2024 16:41:15 +0200 Subject: [PATCH 1/4] Treat Dafny project files as a different VSCode language, so they do not get incorrect syntax highlighting --- package.json | 10 +++++++++- src/language/dafnyLanguageClient.ts | 6 +++++- 2 files changed, 14 insertions(+), 2 deletions(-) diff --git a/package.json b/package.json index 72fd4fe..b871321 100644 --- a/package.json +++ b/package.json @@ -123,7 +123,15 @@ ], "extensions": [ ".dfy", - ".dfyi", + ".dfyi" + ], + "configuration": "./language-configuration.json" + }, { + "id": "dafnyProject", + "aliases": [ + "Dafny Project file" + ], + "extensions": [ "dfyconfig.toml" ], "configuration": "./language-configuration.json" diff --git a/src/language/dafnyLanguageClient.ts b/src/language/dafnyLanguageClient.ts index dd08ec3..ee2a863 100644 --- a/src/language/dafnyLanguageClient.ts +++ b/src/language/dafnyLanguageClient.ts @@ -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', + language: 'dafnyProject' + } + ], diagnosticCollectionName: LanguageServerId, middleware: { handleDiagnostics: (uri: Uri, diagnostics: Diagnostic[], next: HandleDiagnosticsSignature) => { From cb70fa0d24afef6855c193422c2c6ec55c051b8c Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 7 May 2024 17:14:43 +0200 Subject: [PATCH 2/4] Add syntaxes --- .vscode/launch.json | 30 ++ ....json => dafny-language-configuration.json | 0 package.json | 11 +- project-language-configuration.json | 40 ++ syntaxes/toml.tmLanguage.json | 343 ++++++++++++++++++ 5 files changed, 421 insertions(+), 3 deletions(-) rename language-configuration.json => dafny-language-configuration.json (100%) create mode 100644 project-language-configuration.json create mode 100644 syntaxes/toml.tmLanguage.json diff --git a/.vscode/launch.json b/.vscode/launch.json index 9f1ee96..d1d730f 100644 --- a/.vscode/launch.json +++ b/.vscode/launch.json @@ -33,6 +33,36 @@ ], "preLaunchTask": "${defaultBuildTask}" }, + { + "name": "Run with $DAFNY_DEV_SERVER2", + "type": "extensionHost", + "request": "launch", + "args": [ + "--extensionDevelopmentPath=${workspaceFolder}" + ], + "env": { + "DAFNY_SERVER_OVERRIDE": "/Users/rwillems/SourceCode/dafny2/Scripts/dafny", + }, + "outFiles": [ + "${workspaceFolder}/dist/**/*.js" + ], + "preLaunchTask": "${defaultBuildTask}" + }, + { + "name": "Run with $DAFNY_DEV_SERVER3", + "type": "extensionHost", + "request": "launch", + "args": [ + "--extensionDevelopmentPath=${workspaceFolder}" + ], + "env": { + "DAFNY_SERVER_OVERRIDE": "/Users/rwillems/SourceCode/dafny3/Scripts/dafny", + }, + "outFiles": [ + "${workspaceFolder}/dist/**/*.js" + ], + "preLaunchTask": "${defaultBuildTask}" + }, { "name": "Extension Tests", "type": "extensionHost", diff --git a/language-configuration.json b/dafny-language-configuration.json similarity index 100% rename from language-configuration.json rename to dafny-language-configuration.json diff --git a/package.json b/package.json index b871321..4ffb019 100644 --- a/package.json +++ b/package.json @@ -125,7 +125,7 @@ ".dfy", ".dfyi" ], - "configuration": "./language-configuration.json" + "configuration": "./dafny-language-configuration.json" }, { "id": "dafnyProject", "aliases": [ @@ -134,7 +134,7 @@ "extensions": [ "dfyconfig.toml" ], - "configuration": "./language-configuration.json" + "configuration": "./project-language-configuration.json" } ], "grammars": [ @@ -142,7 +142,12 @@ "language": "dafny", "scopeName": "text.dfy.dafny", "path": "./syntaxes/Dafny.tmLanguage" - } + }, + // { + // "language": "dafnyProject", + // "scopeName": "source.toml", + // "path": "./syntaxes/toml.tmLanguage.json" + // } ], "configuration": { "type": "object", diff --git a/project-language-configuration.json b/project-language-configuration.json new file mode 100644 index 0000000..494cbe1 --- /dev/null +++ b/project-language-configuration.json @@ -0,0 +1,40 @@ +{ + "comments": { + "lineComment": "#" + }, + "autoCloseBefore": ";:.,=}])> \n\t", + "brackets": [ + [ + "[", + "]" + ] + ], + "autoClosingPairs": [ + { "open": "\"", "close": "\"", "notIn": ["string"] }, + { "open": "'", "close": "'", "notIn": ["string", "comment"] }, + { "open": "[", "close": "]" }, + { "open": "{", "close": "}" } + ], + "surroundingPairs": [ + [ + "\"", + "\"" + ], + [ + "'", + "'" + ], + [ + "(", + ")" + ], + [ + "[", + "]" + ], + [ + "{", + "}" + ] + ] +} \ No newline at end of file diff --git a/syntaxes/toml.tmLanguage.json b/syntaxes/toml.tmLanguage.json new file mode 100644 index 0000000..8d15846 --- /dev/null +++ b/syntaxes/toml.tmLanguage.json @@ -0,0 +1,343 @@ +{ + "version": "1.0.0", + "scopeName": "source.toml", + "uuid": "8b4e5008-c50d-11ea-a91b-54ee75aeeb97", + "information_for_contributors": [ + "Originally was maintained by aster (galaster@foxmail.com). This notice is only kept here for the record, please don't send e-mails about bugs and other issues." + ], + "patterns": [ + { + "include": "#commentDirective" + }, + { + "include": "#comment" + }, + { + "include": "#table" + }, + { + "include": "#entryBegin" + }, + { + "include": "#value" + } + ], + "repository": { + "comment": { + "captures": { + "1": { + "name": "comment.line.number-sign.toml" + }, + "2": { + "name": "punctuation.definition.comment.toml" + } + }, + "comment": "Comments", + "match": "\\s*((#).*)$" + }, + "commentDirective": { + "captures": { + "1": { + "name": "meta.preprocessor.toml" + }, + "2": { + "name": "punctuation.definition.meta.preprocessor.toml" + } + }, + "comment": "Comments", + "match": "\\s*((#):.*)$" + }, + "table": { + "patterns": [ + { + "name": "meta.table.toml", + "match": "^\\s*(\\[)\\s*((?:(?:(?:[A-Za-z0-9_+-]+)|(?:\"[^\"]+\")|(?:'[^']+'))\\s*\\.?\\s*)+)\\s*(\\])", + "captures": { + "1": { + "name": "punctuation.definition.table.toml" + }, + "2": { + "patterns": [ + { + "match": "(?:[A-Za-z0-9_+-]+)|(?:\"[^\"]+\")|(?:'[^']+')", + "name": "support.type.property-name.table.toml" + }, + { + "match": "\\.", + "name": "punctuation.separator.dot.toml" + } + ] + }, + "3": { + "name": "punctuation.definition.table.toml" + } + } + }, + { + "name": "meta.array.table.toml", + "match": "^\\s*(\\[\\[)\\s*((?:(?:(?:[A-Za-z0-9_+-]+)|(?:\"[^\"]+\")|(?:'[^']+'))\\s*\\.?\\s*)+)\\s*(\\]\\])", + "captures": { + "1": { + "name": "punctuation.definition.array.table.toml" + }, + "2": { + "patterns": [ + { + "match": "(?:[A-Za-z0-9_+-]+)|(?:\"[^\"]+\")|(?:'[^']+')", + "name": "support.type.property-name.array.toml" + }, + { + "match": "\\.", + "name": "punctuation.separator.dot.toml" + } + ] + }, + "3": { + "name": "punctuation.definition.array.table.toml" + } + } + }, + { + "begin": "(\\{)", + "end": "(\\})", + "name": "meta.table.inline.toml", + "beginCaptures": { + "1": { + "name": "punctuation.definition.table.inline.toml" + } + }, + "endCaptures": { + "1": { + "name": "punctuation.definition.table.inline.toml" + } + }, + "patterns": [ + { + "include": "#comment" + }, + { + "match": ",", + "name": "punctuation.separator.table.inline.toml" + }, + { + "include": "#entryBegin" + }, + { + "include": "#value" + } + ] + } + ] + }, + "entryBegin": { + "name": "meta.entry.toml", + "match": "\\s*((?:(?:(?:[A-Za-z0-9_+-]+)|(?:\"[^\"]+\")|(?:'[^']+'))\\s*\\.?\\s*)+)\\s*(=)", + "captures": { + "1": { + "patterns": [ + { + "match": "(?:[A-Za-z0-9_+-]+)|(?:\"[^\"]+\")|(?:'[^']+')", + "name": "support.type.property-name.toml" + }, + { + "match": "\\.", + "name": "punctuation.separator.dot.toml" + } + ] + }, + "2": { + "name": "punctuation.eq.toml" + } + } + }, + "value": { + "patterns": [ + { + "name": "string.quoted.triple.basic.block.toml", + "begin": "\"\"\"", + "end": "\"\"\"", + "patterns": [ + { + "match": "\\\\([btnfr\"\\\\\\n/ ]|u[0-9A-Fa-f]{4}|U[0-9A-Fa-f]{8})", + "name": "constant.character.escape.toml" + }, + { + "match": "\\\\[^btnfr/\"\\\\\\n]", + "name": "invalid.illegal.escape.toml" + } + ] + }, + { + "name": "string.quoted.single.basic.line.toml", + "begin": "\"", + "end": "\"", + "patterns": [ + { + "match": "\\\\([btnfr\"\\\\\\n/ ]|u[0-9A-Fa-f]{4}|U[0-9A-Fa-f]{8})", + "name": "constant.character.escape.toml" + }, + { + "match": "\\\\[^btnfr/\"\\\\\\n]", + "name": "invalid.illegal.escape.toml" + } + ] + }, + { + "name": "string.quoted.triple.literal.block.toml", + "begin": "'''", + "end": "'''" + }, + { + "name": "string.quoted.single.literal.line.toml", + "begin": "'", + "end": "'" + }, + { + "captures": { + "1": { + "name": "constant.other.time.datetime.offset.toml" + } + }, + "match": "(? Date: Wed, 8 May 2024 11:47:16 +0200 Subject: [PATCH 3/4] Remove unnecessary things --- package.json | 20 +- project-language-configuration.json | 40 ---- src/language/dafnyLanguageClient.ts | 2 +- syntaxes/toml.tmLanguage.json | 343 ---------------------------- 4 files changed, 5 insertions(+), 400 deletions(-) delete mode 100644 project-language-configuration.json delete mode 100644 syntaxes/toml.tmLanguage.json diff --git a/package.json b/package.json index 4ffb019..9acf955 100644 --- a/package.json +++ b/package.json @@ -11,6 +11,9 @@ "bugs": { "url": "https://github.com/dafny-lang/ide-vscode/issues" }, + "activationEvents": [ + "onLanguage:toml" + ], "qna": false, "license": "MIT", "galleryBanner": { @@ -126,15 +129,6 @@ ".dfyi" ], "configuration": "./dafny-language-configuration.json" - }, { - "id": "dafnyProject", - "aliases": [ - "Dafny Project file" - ], - "extensions": [ - "dfyconfig.toml" - ], - "configuration": "./project-language-configuration.json" } ], "grammars": [ @@ -142,12 +136,7 @@ "language": "dafny", "scopeName": "text.dfy.dafny", "path": "./syntaxes/Dafny.tmLanguage" - }, - // { - // "language": "dafnyProject", - // "scopeName": "source.toml", - // "path": "./syntaxes/toml.tmLanguage.json" - // } + } ], "configuration": { "type": "object", @@ -322,7 +311,6 @@ } ] }, - "activationEvents": [], "scripts": { "vscode:prepublish": "npm run package", "compile": "webpack", diff --git a/project-language-configuration.json b/project-language-configuration.json deleted file mode 100644 index 494cbe1..0000000 --- a/project-language-configuration.json +++ /dev/null @@ -1,40 +0,0 @@ -{ - "comments": { - "lineComment": "#" - }, - "autoCloseBefore": ";:.,=}])> \n\t", - "brackets": [ - [ - "[", - "]" - ] - ], - "autoClosingPairs": [ - { "open": "\"", "close": "\"", "notIn": ["string"] }, - { "open": "'", "close": "'", "notIn": ["string", "comment"] }, - { "open": "[", "close": "]" }, - { "open": "{", "close": "}" } - ], - "surroundingPairs": [ - [ - "\"", - "\"" - ], - [ - "'", - "'" - ], - [ - "(", - ")" - ], - [ - "[", - "]" - ], - [ - "{", - "}" - ] - ] -} \ No newline at end of file diff --git a/src/language/dafnyLanguageClient.ts b/src/language/dafnyLanguageClient.ts index ee2a863..5a19fb0 100644 --- a/src/language/dafnyLanguageClient.ts +++ b/src/language/dafnyLanguageClient.ts @@ -154,7 +154,7 @@ export class DafnyLanguageClient extends LanguageClient { const clientOptions: LanguageClientOptions = { documentSelector: [ DafnyDocumentFilter, { scheme: 'file', - language: 'dafnyProject' + pattern: '**/*dfyconfig.toml' } ], diagnosticCollectionName: LanguageServerId, diff --git a/syntaxes/toml.tmLanguage.json b/syntaxes/toml.tmLanguage.json deleted file mode 100644 index 8d15846..0000000 --- a/syntaxes/toml.tmLanguage.json +++ /dev/null @@ -1,343 +0,0 @@ -{ - "version": "1.0.0", - "scopeName": "source.toml", - "uuid": "8b4e5008-c50d-11ea-a91b-54ee75aeeb97", - "information_for_contributors": [ - "Originally was maintained by aster (galaster@foxmail.com). This notice is only kept here for the record, please don't send e-mails about bugs and other issues." - ], - "patterns": [ - { - "include": "#commentDirective" - }, - { - "include": "#comment" - }, - { - "include": "#table" - }, - { - "include": "#entryBegin" - }, - { - "include": "#value" - } - ], - "repository": { - "comment": { - "captures": { - "1": { - "name": "comment.line.number-sign.toml" - }, - "2": { - "name": "punctuation.definition.comment.toml" - } - }, - "comment": "Comments", - "match": "\\s*((#).*)$" - }, - "commentDirective": { - "captures": { - "1": { - "name": "meta.preprocessor.toml" - }, - "2": { - "name": "punctuation.definition.meta.preprocessor.toml" - } - }, - "comment": "Comments", - "match": "\\s*((#):.*)$" - }, - "table": { - "patterns": [ - { - "name": "meta.table.toml", - "match": "^\\s*(\\[)\\s*((?:(?:(?:[A-Za-z0-9_+-]+)|(?:\"[^\"]+\")|(?:'[^']+'))\\s*\\.?\\s*)+)\\s*(\\])", - "captures": { - "1": { - "name": "punctuation.definition.table.toml" - }, - "2": { - "patterns": [ - { - "match": "(?:[A-Za-z0-9_+-]+)|(?:\"[^\"]+\")|(?:'[^']+')", - "name": "support.type.property-name.table.toml" - }, - { - "match": "\\.", - "name": "punctuation.separator.dot.toml" - } - ] - }, - "3": { - "name": "punctuation.definition.table.toml" - } - } - }, - { - "name": "meta.array.table.toml", - "match": "^\\s*(\\[\\[)\\s*((?:(?:(?:[A-Za-z0-9_+-]+)|(?:\"[^\"]+\")|(?:'[^']+'))\\s*\\.?\\s*)+)\\s*(\\]\\])", - "captures": { - "1": { - "name": "punctuation.definition.array.table.toml" - }, - "2": { - "patterns": [ - { - "match": "(?:[A-Za-z0-9_+-]+)|(?:\"[^\"]+\")|(?:'[^']+')", - "name": "support.type.property-name.array.toml" - }, - { - "match": "\\.", - "name": "punctuation.separator.dot.toml" - } - ] - }, - "3": { - "name": "punctuation.definition.array.table.toml" - } - } - }, - { - "begin": "(\\{)", - "end": "(\\})", - "name": "meta.table.inline.toml", - "beginCaptures": { - "1": { - "name": "punctuation.definition.table.inline.toml" - } - }, - "endCaptures": { - "1": { - "name": "punctuation.definition.table.inline.toml" - } - }, - "patterns": [ - { - "include": "#comment" - }, - { - "match": ",", - "name": "punctuation.separator.table.inline.toml" - }, - { - "include": "#entryBegin" - }, - { - "include": "#value" - } - ] - } - ] - }, - "entryBegin": { - "name": "meta.entry.toml", - "match": "\\s*((?:(?:(?:[A-Za-z0-9_+-]+)|(?:\"[^\"]+\")|(?:'[^']+'))\\s*\\.?\\s*)+)\\s*(=)", - "captures": { - "1": { - "patterns": [ - { - "match": "(?:[A-Za-z0-9_+-]+)|(?:\"[^\"]+\")|(?:'[^']+')", - "name": "support.type.property-name.toml" - }, - { - "match": "\\.", - "name": "punctuation.separator.dot.toml" - } - ] - }, - "2": { - "name": "punctuation.eq.toml" - } - } - }, - "value": { - "patterns": [ - { - "name": "string.quoted.triple.basic.block.toml", - "begin": "\"\"\"", - "end": "\"\"\"", - "patterns": [ - { - "match": "\\\\([btnfr\"\\\\\\n/ ]|u[0-9A-Fa-f]{4}|U[0-9A-Fa-f]{8})", - "name": "constant.character.escape.toml" - }, - { - "match": "\\\\[^btnfr/\"\\\\\\n]", - "name": "invalid.illegal.escape.toml" - } - ] - }, - { - "name": "string.quoted.single.basic.line.toml", - "begin": "\"", - "end": "\"", - "patterns": [ - { - "match": "\\\\([btnfr\"\\\\\\n/ ]|u[0-9A-Fa-f]{4}|U[0-9A-Fa-f]{8})", - "name": "constant.character.escape.toml" - }, - { - "match": "\\\\[^btnfr/\"\\\\\\n]", - "name": "invalid.illegal.escape.toml" - } - ] - }, - { - "name": "string.quoted.triple.literal.block.toml", - "begin": "'''", - "end": "'''" - }, - { - "name": "string.quoted.single.literal.line.toml", - "begin": "'", - "end": "'" - }, - { - "captures": { - "1": { - "name": "constant.other.time.datetime.offset.toml" - } - }, - "match": "(? Date: Wed, 8 May 2024 11:48:46 +0200 Subject: [PATCH 4/4] Remove garbage --- .vscode/launch.json | 30 ------------------------------ 1 file changed, 30 deletions(-) diff --git a/.vscode/launch.json b/.vscode/launch.json index d1d730f..9f1ee96 100644 --- a/.vscode/launch.json +++ b/.vscode/launch.json @@ -33,36 +33,6 @@ ], "preLaunchTask": "${defaultBuildTask}" }, - { - "name": "Run with $DAFNY_DEV_SERVER2", - "type": "extensionHost", - "request": "launch", - "args": [ - "--extensionDevelopmentPath=${workspaceFolder}" - ], - "env": { - "DAFNY_SERVER_OVERRIDE": "/Users/rwillems/SourceCode/dafny2/Scripts/dafny", - }, - "outFiles": [ - "${workspaceFolder}/dist/**/*.js" - ], - "preLaunchTask": "${defaultBuildTask}" - }, - { - "name": "Run with $DAFNY_DEV_SERVER3", - "type": "extensionHost", - "request": "launch", - "args": [ - "--extensionDevelopmentPath=${workspaceFolder}" - ], - "env": { - "DAFNY_SERVER_OVERRIDE": "/Users/rwillems/SourceCode/dafny3/Scripts/dafny", - }, - "outFiles": [ - "${workspaceFolder}/dist/**/*.js" - ], - "preLaunchTask": "${defaultBuildTask}" - }, { "name": "Extension Tests", "type": "extensionHost",