Skip to content

Commit

Permalink
[vscode] Expand selectors to include vscode-vfs:// URIs
Browse files Browse the repository at this point in the history
This is used in `github.dev`; we also document limited virtual
workspace support.
  • Loading branch information
ejgallego committed Oct 4, 2024
1 parent 7bb1202 commit b9de650
Show file tree
Hide file tree
Showing 6 changed files with 37 additions and 6 deletions.
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
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
13 changes: 12 additions & 1 deletion editor/code/src/config.ts
Original file line number Diff line number Diff line change
@@ -1,4 +1,7 @@
import { TextDocumentFilter } from "vscode-languageclient";
import {
SelectedCompletionInfo,
TextDocumentFilter,
} from "vscode-languageclient";

export interface CoqLspServerConfig {
client_version: string;
Expand Down Expand Up @@ -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);
}
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 *)
(************************************************************************)

0 comments on commit b9de650

Please sign in to comment.