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.

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

[vscode] Expand selectors to include vscode-vfs:// URIs #849

Merged
merged 1 commit into from
Oct 4, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
7 changes: 7 additions & 0 deletions CHANGES.md
Original file line number Diff line number Diff line change
@@ -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 !
------------------------

Expand Down
7 changes: 7 additions & 0 deletions editor/code/CHANGELOG.md
Original file line number Diff line number Diff line change
@@ -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 !
------------------------

Expand Down
4 changes: 2 additions & 2 deletions editor/code/package-lock.json

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

8 changes: 7 additions & 1 deletion editor/code/package.json
Original file line number Diff line number Diff line change
Expand Up @@ -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 <[email protected]>",
"Ali Caglayan <[email protected]>",
Expand Down Expand Up @@ -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": [
{
Expand Down
6 changes: 3 additions & 3 deletions editor/code/src/client.ts
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -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 =
Expand Down Expand Up @@ -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();
Expand Down
8 changes: 8 additions & 0 deletions editor/code/src/config.ts
Original file line number Diff line number Diff line change
Expand Up @@ -96,4 +96,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);
}
2 changes: 1 addition & 1 deletion fleche/version.ml
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,6 @@ type t = string

(************************************************************************)
(* UPDATE VERSION HERE *)
let server = "0.2.1"
let server = "0.2.2"
(* UPDATE VERSION HERE *)
(************************************************************************)