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.ts48
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);
}
};
}