Unnamed repository; edit this file 'description' to name the repository.
Diffstat (limited to 'editors/code/src/commands.ts')
| -rw-r--r-- | editors/code/src/commands.ts | 48 |
1 files changed, 45 insertions, 3 deletions
diff --git a/editors/code/src/commands.ts b/editors/code/src/commands.ts index 245557b1e8..7e24de664e 100644 --- a/editors/code/src/commands.ts +++ b/editors/code/src/commands.ts @@ -21,6 +21,7 @@ import type { LanguageClient } from "vscode-languageclient/node"; import { LINKED_COMMANDS } from "./client"; import type { DependencyId } from "./dependencies_provider"; import { unwrapUndefinable } from "./undefinable"; +import { log } from "./util"; export * from "./ast_inspector"; export * from "./run"; @@ -947,10 +948,51 @@ export function openDocs(ctx: CtxInit): Cmd { const position = editor.selection.active; const textDocument = { uri: editor.document.uri.toString() }; - const doclink = await client.sendRequest(ra.openDocs, { position, textDocument }); + const docLinks = await client.sendRequest(ra.openDocs, { position, textDocument }); + log.debug(docLinks); - if (doclink != null) { - await vscode.commands.executeCommand("vscode.open", vscode.Uri.parse(doclink)); + let fileType = vscode.FileType.Unknown; + if (docLinks.local !== undefined) { + try { + fileType = (await vscode.workspace.fs.stat(vscode.Uri.parse(docLinks.local))).type; + } catch (e) { + log.debug("stat() threw error. Falling back to web version", e); + } + } + + let docLink = fileType & vscode.FileType.File ? docLinks.local : docLinks.web; + if (docLink) { + // instruct vscode to handle the vscode-remote link directly + if (docLink.startsWith("vscode-remote://")) { + docLink = docLink.replace("vscode-remote://", "vscode://vscode-remote/"); + } + const docUri = vscode.Uri.parse(docLink); + await vscode.env.openExternal(docUri); + } + }; +} + +export function openExternalDocs(ctx: CtxInit): Cmd { + return async () => { + const editor = vscode.window.activeTextEditor; + if (!editor) { + return; + } + const client = ctx.client; + + const position = editor.selection.active; + const textDocument = { uri: editor.document.uri.toString() }; + + const docLinks = await client.sendRequest(ra.openDocs, { position, textDocument }); + + let docLink = docLinks.web; + if (docLink) { + // instruct vscode to handle the vscode-remote link directly + if (docLink.startsWith("vscode-remote://")) { + docLink = docLink.replace("vscode-remote://", "vscode://vscode-remote/"); + } + const docUri = vscode.Uri.parse(docLink); + await vscode.env.openExternal(docUri); } }; } |