From 55bae646f19c39bebb010185d066122ae2e16950 Mon Sep 17 00:00:00 2001 From: Will Thomas <30wthomas@gmail.com> Date: Tue, 10 Sep 2024 13:02:10 -0500 Subject: [PATCH 1/4] Making vscoq activity bar logo appear only when coq files present --- client/package.json | 3 ++- client/src/extension.ts | 21 +++++++++++++++++++++ 2 files changed, 23 insertions(+), 1 deletion(-) diff --git a/client/package.json b/client/package.json index 2c0a950d..bce0a808 100644 --- a/client/package.json +++ b/client/package.json @@ -73,7 +73,8 @@ { "type": "webview", "id": "vscoq.search", - "name": "Query" + "name": "Query", + "when": "coqFilesPresent" } ] }, diff --git a/client/src/extension.ts b/client/src/extension.ts index 8dd34474..9ab04809 100644 --- a/client/src/extension.ts +++ b/client/src/extension.ts @@ -51,6 +51,27 @@ import { QUICKFIX_COMMAND, CoqWarningQuickFix } from './QuickFixProvider'; let client: Client; export function activate(context: ExtensionContext) { + + // Function to check for Coq files present in the workspace + function checkCoqFilesPresent() { + if (workspace.workspaceFolders) { + // Search for Coq files (*.v) in the current workspace + workspace.findFiles('**/*.v').then(files => { + const hasCoqFiles = files.length > 0; + commands.executeCommand('setContext', 'coqFilesPresent', hasCoqFiles); + }); + } else { + commands.executeCommand('setContext', 'coqFilesPresent', false); + } + } + + // Set initially on extension activation + checkCoqFilesPresent(); + + // Watch for changes to the workspace and files being added or removed + workspace.onDidChangeWorkspaceFolders(checkCoqFilesPresent); + workspace.onDidCreateFiles(checkCoqFilesPresent); + workspace.onDidDeleteFiles(checkCoqFilesPresent); const coqTM = new VsCoqToolchainManager(); coqTM.intialize().then( From 43d346ecaeaea0d929a4deee3af77d8867847391 Mon Sep 17 00:00:00 2001 From: Will Thomas <30wthomas@gmail.com> Date: Thu, 12 Sep 2024 12:10:51 -0500 Subject: [PATCH 2/4] Adding _CoqProject language entry and tracking them for activity bar display --- client/coq-project.configuration.json | 5 ++++ client/package.json | 25 ++++++++++++++++-- client/src/extension.ts | 28 +++++++------------- client/syntax/coq-project.tmLanguage.json | 32 +++++++++++++++++++++++ 4 files changed, 70 insertions(+), 20 deletions(-) create mode 100644 client/coq-project.configuration.json create mode 100644 client/syntax/coq-project.tmLanguage.json diff --git a/client/coq-project.configuration.json b/client/coq-project.configuration.json new file mode 100644 index 00000000..1b7cf3bd --- /dev/null +++ b/client/coq-project.configuration.json @@ -0,0 +1,5 @@ +{ + "comments": { + "lineComment": "#" + } +} \ No newline at end of file diff --git a/client/package.json b/client/package.json index bce0a808..2c372f3a 100644 --- a/client/package.json +++ b/client/package.json @@ -29,7 +29,8 @@ "bugs": "https://github.com/coq-community/vscoq/issues", "homepage": "https://github.com/coq-community/vscoq/blob/master/README.md", "activationEvents": [ - "onLanguage:coq" + "workspaceContains:**/_CoqProject", + "workspaceContains:**/*.v" ], "main": "./dist/extension.js", "contributes": { @@ -50,6 +51,21 @@ "light": "./assets/logo.png", "dark": "./assets/logo.png" } + }, + { + "id": "coq-project", + "aliases": [ + "Coq Project", + "coq-project" + ], + "extensions": [ + "_CoqProject" + ], + "configuration": "./coq-project.configuration.json", + "icon": { + "light": "./assets/logo.png", + "dark": "./assets/logo.png" + } } ], "grammars": [ @@ -57,6 +73,11 @@ "language": "coq", "scopeName": "source.coq", "path": "./syntax/coq.tmLanguage.json" + }, + { + "language": "coq-project", + "scopeName": "source.coq-project", + "path": "./syntax/coq-project.tmLanguage.json" } ], "viewsContainers": { @@ -74,7 +95,7 @@ "type": "webview", "id": "vscoq.search", "name": "Query", - "when": "coqFilesPresent" + "when": "inCoqProject" } ] }, diff --git a/client/src/extension.ts b/client/src/extension.ts index 9ab04809..9e534e18 100644 --- a/client/src/extension.ts +++ b/client/src/extension.ts @@ -51,27 +51,17 @@ import { QUICKFIX_COMMAND, CoqWarningQuickFix } from './QuickFixProvider'; let client: Client; export function activate(context: ExtensionContext) { + commands.executeCommand('setContext', 'inCoqProject', true); - // Function to check for Coq files present in the workspace - function checkCoqFilesPresent() { - if (workspace.workspaceFolders) { - // Search for Coq files (*.v) in the current workspace - workspace.findFiles('**/*.v').then(files => { - const hasCoqFiles = files.length > 0; - commands.executeCommand('setContext', 'coqFilesPresent', hasCoqFiles); + function checkInCoqProject() { + workspace.findFiles('**/{*.v,_CoqProject}').then(files => { + commands.executeCommand('setContext', 'inCoqProject', files.length > 0); }); - } else { - commands.executeCommand('setContext', 'coqFilesPresent', false); - } } - // Set initially on extension activation - checkCoqFilesPresent(); - - // Watch for changes to the workspace and files being added or removed - workspace.onDidChangeWorkspaceFolders(checkCoqFilesPresent); - workspace.onDidCreateFiles(checkCoqFilesPresent); - workspace.onDidDeleteFiles(checkCoqFilesPresent); + // Watch for files being added or removed + workspace.onDidCreateFiles(checkInCoqProject); + workspace.onDidDeleteFiles(checkInCoqProject); const coqTM = new VsCoqToolchainManager(); coqTM.intialize().then( @@ -403,4 +393,6 @@ Path: \`${coqTM.getVsCoqTopPath()}\` } // This method is called when your extension is deactivated -export function deactivate() {} +export function deactivate() { + commands.executeCommand('setContext', 'inCoqProject', undefined); +} diff --git a/client/syntax/coq-project.tmLanguage.json b/client/syntax/coq-project.tmLanguage.json new file mode 100644 index 00000000..d7465a5c --- /dev/null +++ b/client/syntax/coq-project.tmLanguage.json @@ -0,0 +1,32 @@ +{ + "fileTypes": [ + "_CoqProject" + ], + "name": "Coq Project", + "scopeName": "source.coq-project", + "patterns": [ + { + "name": "comment.line.coq-project", + "match": "#.*$" + }, + { + "name": "string.quoted.double.coq-project", + "begin": "\"", + "end": "\"" + }, + { + "name": "keyword.other.coq-project", + "match": "(-arg|-generate-meta-for-package|-docroot|-Q|-R|-I|-native-compiler)" + }, + { + "name": "entity.name.file.coq-project", + "match": "(.*(\\|/))?(\\S+\\.v)" + }, + { + "name": "entity.name.folder.coq-project", + "match": "(.*(\\|/))?(\\S+)" + } + ], + "repository": {}, + "uuid": "94440acd-57c4-46ad-b59b-d05ab6902361" +} \ No newline at end of file From 8069e2e2f1c436d043b5c12d86429484d6617d8e Mon Sep 17 00:00:00 2001 From: Will Thomas <30wthomas@gmail.com> Date: Thu, 12 Sep 2024 12:15:16 -0500 Subject: [PATCH 3/4] Cleaner approach where if all coqfiles are deleted bar remains until refresh --- client/src/extension.ts | 10 ---------- 1 file changed, 10 deletions(-) diff --git a/client/src/extension.ts b/client/src/extension.ts index 9e534e18..15d3ed87 100644 --- a/client/src/extension.ts +++ b/client/src/extension.ts @@ -52,16 +52,6 @@ let client: Client; export function activate(context: ExtensionContext) { commands.executeCommand('setContext', 'inCoqProject', true); - - function checkInCoqProject() { - workspace.findFiles('**/{*.v,_CoqProject}').then(files => { - commands.executeCommand('setContext', 'inCoqProject', files.length > 0); - }); - } - - // Watch for files being added or removed - workspace.onDidCreateFiles(checkInCoqProject); - workspace.onDidDeleteFiles(checkInCoqProject); const coqTM = new VsCoqToolchainManager(); coqTM.intialize().then( From 24fb030ab549927f45c0d8e44bfa7b2ccab3dcbb Mon Sep 17 00:00:00 2001 From: Will Thomas <30wthomas@gmail.com> Date: Thu, 12 Sep 2024 12:10:51 -0500 Subject: [PATCH 4/4] Calling checkInCoqProject whenever files are created or deleted --- client/src/extension.ts | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/client/src/extension.ts b/client/src/extension.ts index 15d3ed87..9e534e18 100644 --- a/client/src/extension.ts +++ b/client/src/extension.ts @@ -52,6 +52,16 @@ let client: Client; export function activate(context: ExtensionContext) { commands.executeCommand('setContext', 'inCoqProject', true); + + function checkInCoqProject() { + workspace.findFiles('**/{*.v,_CoqProject}').then(files => { + commands.executeCommand('setContext', 'inCoqProject', files.length > 0); + }); + } + + // Watch for files being added or removed + workspace.onDidCreateFiles(checkInCoqProject); + workspace.onDidDeleteFiles(checkInCoqProject); const coqTM = new VsCoqToolchainManager(); coqTM.intialize().then(