vscode: Support opening local documentation if available

Displaying local instead of web docs can have many benefits:
- the web version may have different features enabled than locally selected
- the standard library may be a different version than is available online
- the user may not be online and therefore cannot access the web documentation
- the documentation may not be available online at all, for example because it
  is for a new feature in a library the user is currently developing

If the documentation is not available locally, the extension still falls back to
the web version.

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,7 +948,24 @@ 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 });
+
+        let fileType = vscode.FileType.Unknown;
+        if (typeof doclinks.local === "string") {
+            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;
+        if (fileType & vscode.FileType.File) {
+            // file does exist locally
+            doclink = doclinks.local;
+        } else {
+            doclink = doclinks.web;
+        }
 
         if (doclink != null) {
             await vscode.env.openExternal(vscode.Uri.parse(doclink));