From b9de650fc3b0bb416359e082f67c0febb11fd9f4 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 4 Oct 2024 18:20:42 +0200 Subject: [PATCH] [vscode] Expand selectors to include `vscode-vfs://` URIs This is used in `github.dev`; we also document limited virtual workspace support. --- CHANGES.md | 7 +++++++ editor/code/CHANGELOG.md | 7 +++++++ editor/code/package.json | 8 +++++++- editor/code/src/client.ts | 6 +++--- editor/code/src/config.ts | 13 ++++++++++++- fleche/version.ml | 2 +- 6 files changed, 37 insertions(+), 6 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index 02f85218c..02225c39a 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,3 +1,10 @@ +# coq-lsp 0.2.2: To Virtual or not To Virtual +--------------------------------------------- + + - [vscode] Expand selectors to include `vscode-vfs://` URIs used in + `github.dev`, document limited virtual workspace support in + `package.json` (@ejgallego, #849) + # coq-lsp 0.2.1: Click ! ------------------------ diff --git a/editor/code/CHANGELOG.md b/editor/code/CHANGELOG.md index a11be8f2b..0eab4ec0d 100644 --- a/editor/code/CHANGELOG.md +++ b/editor/code/CHANGELOG.md @@ -1,3 +1,10 @@ +# coq-lsp 0.2.2: To Virtual or not To Virtual +--------------------------------------------- + + - [vscode] Expand selectors to include `vscode-vfs://` URIs used in + `github.dev`, document limited virtual workspace support in + `package.json` (@ejgallego, #849) + # coq-lsp 0.2.1: Click ! ------------------------ diff --git a/editor/code/package.json b/editor/code/package.json index 247188f09..de6ce5c0b 100644 --- a/editor/code/package.json +++ b/editor/code/package.json @@ -2,7 +2,7 @@ "name": "coq-lsp", "displayName": "Coq LSP", "description": "Coq LSP provides native vsCode support for checking Coq proof documents", - "version": "0.2.1", + "version": "0.2.2", "contributors": [ "Emilio Jesús Gallego Arias ", "Ali Caglayan ", @@ -32,6 +32,12 @@ "onLanguage:markdown", "onLanguage:latex" ], + "capabilities": { + "virtualWorkspaces": { + "supported": "limited", + "description": "File operations such as jump to definition are not supported in virtual workspaces. While almost fully functional, coq-lsp remains experiemental as a Web Extension." + } + }, "contributes": { "languages": [ { diff --git a/editor/code/src/client.ts b/editor/code/src/client.ts index d8dbf3522..29faaf89f 100644 --- a/editor/code/src/client.ts +++ b/editor/code/src/client.ts @@ -210,7 +210,7 @@ export function activateCoqLSP( const initializationOptions: CoqLspServerConfig = configDidChange(wsConfig); const clientOptions: LanguageClientOptions = { - documentSelector: CoqSelector.local, + documentSelector: CoqSelector.owned, outputChannelName: "Coq LSP Server Events", revealOutputChannelOn: RevealOutputChannelOn.Info, initializationOptions, @@ -335,7 +335,7 @@ export function activateCoqLSP( let textDocument = { uri, version }; infoPanel.notifyLackOfVSLS(textDocument, position); return; - } else if (languages.match(CoqSelector.local, textEditor.document) < 1) + } else if (languages.match(CoqSelector.owned, textEditor.document) < 1) return; const kind = @@ -373,7 +373,7 @@ export function activateCoqLSP( if ( config.check_on_scroll && serverConfig.check_only_on_request && - languages.match(CoqSelector.local, evt.textEditor.document) > 0 && + languages.match(CoqSelector.owned, evt.textEditor.document) > 0 && evt.visibleRanges[0] ) { let uri = evt.textEditor.document.uri.toString(); diff --git a/editor/code/src/config.ts b/editor/code/src/config.ts index a55320fca..44ceed12c 100644 --- a/editor/code/src/config.ts +++ b/editor/code/src/config.ts @@ -1,4 +1,7 @@ -import { TextDocumentFilter } from "vscode-languageclient"; +import { + SelectedCompletionInfo, + TextDocumentFilter, +} from "vscode-languageclient"; export interface CoqLspServerConfig { client_version: string; @@ -96,4 +99,12 @@ export namespace CoqSelector { export const vsls: TextDocumentFilter[] = all.map((selector) => { return { ...selector, scheme: "vsls" }; }); + + // Virtual workspaces such as github.dev + export const virtual: TextDocumentFilter[] = all.map((selector) => { + return { ...selector, scheme: "vscode-vfs" }; + }); + + // Files that are owned by our server, local + virtual + export const owned: TextDocumentFilter[] = local.concat(virtual); } diff --git a/fleche/version.ml b/fleche/version.ml index c3a588d88..2b22f1f75 100644 --- a/fleche/version.ml +++ b/fleche/version.ml @@ -12,6 +12,6 @@ type t = string (************************************************************************) (* UPDATE VERSION HERE *) -let server = "0.2.1" +let server = "0.2.2" (* UPDATE VERSION HERE *) (************************************************************************)