[code] Enable web extension support.

For now this will not try to start the worker.

Fixes #234

CHANGES.md

@@ -3,10 +3,12 @@
 
  - Improvements and clenaups on hover display, in particular we don't
    print repeated `Notation` strings (@ejgallego, #422)
-
  - Don't fail on missing serlib plugins, they are indeed an
    optimization; this mostly impacts 8.16 by lowering the SerAPI
    requirements (@ejgallego, #421)
+ - Enable web extension support. For now this will not try to start
+   the coq-lsp worker as it is now ready. (@ejgallego, #430, fixes
+   #234)
 
 # coq-lsp 0.1.6: Peek
 ---------------------

CONTRIBUTING.md

@@ -201,6 +201,11 @@ Debug" panel in Visual Studio Code, or the F5 keybinding.
 You can of course install the extension in your `~/.vscode/` folder if so you
 desire, tho this is not recommended.
 
+### Testing the Web Extension
+
+`coq-lsp` has preliminary support to run as a "Web Extension", to test
+that, you want to use the web extension profile in the launch setup.
+
 ### Miscellaneous info
 
 - The "Restart Coq LSP server" command will be of great help while developing

coq/loader.ml

@@ -62,9 +62,9 @@ let map_serlib fl_pkg =
     check_package_exists serlib_name
   else None
 
-(* We are more liberal in the case a SerAPI plugin is not availabe, as
-   the fallbacks are "safe", tho will yield way worse incremental
-   behavior for expressions defined by the plugin *)
+(* We are more liberal in the case a SerAPI plugin is not availabe, as the
+   fallbacks are "safe", tho will yield way worse incremental behavior for
+   expressions defined by the plugin *)
 let safe_loader loader fl_pkg =
   try loader [fl_pkg]
   with

editor/code/.vscode/launch.json

@@ -14,6 +14,19 @@
       "outFiles": ["${workspaceFolder}/out/**/*.js"],
       "preLaunchTask": "${defaultBuildTask}"
     },
+    {
+      "name": "Run Web Extension in VS Code",
+      "type": "extensionHost",
+      "debugWebWorkerHost": true,
+      "request": "launch",
+      "runtimeExecutable": "${execPath}",
+      "args": [
+        "--extensionDevelopmentPath=${workspaceFolder}",
+        "--extensionDevelopmentKind=web"
+      ],
+      "outFiles": ["${workspaceFolder}/out/**/*.js"],
+      "preLaunchTask": "${defaultBuildTask}"
+    },
     {
       "name": "Extension Tests",
       "type": "extensionHost",

editor/code/esbuild.mjs

@@ -24,20 +24,37 @@ let sourcemap_client = disable_sourcemap ? null : { sourcemap: true };
 let sourcemap_view = disable_sourcemap ? null : { sourcemap: "inline" };
 
 // Build of the VS Code extension, for electron (hence cjs + node)
-var client = esbuild
+var node = esbuild
   .build({
-    entryPoints: ["./src/client.ts"],
+    entryPoints: ["./src/node.ts"],
     bundle: true,
     ...sourcemap_client,
     format: "cjs",
     platform: "node",
     external: ["vscode"],
-    outfile: "out/src/client.js",
+    outfile: "out/src/node.js",
     minify,
-    watch: watch("./src/client.ts"),
+    watch: watch("./src/node.ts"),
   })
   .then(() => {
-    console.log("[watch] build finished for ./src/client.ts");
+    console.log("[watch] build finished for ./src/node.ts");
+  })
+  .catch(() => process.exit(1));
+
+var browser = esbuild
+  .build({
+    entryPoints: ["./src/browser.ts"],
+    bundle: true,
+    ...sourcemap_client,
+    format: "cjs",
+    platform: "browser",
+    external: ["vscode"],
+    outfile: "out/src/browser.js",
+    minify,
+    watch: watch("./src/browser.ts"),
+  })
+  .then(() => {
+    console.log("[watch] build finished for ./src/browser.ts");
   })
   .catch(() => process.exit(1));
 
@@ -62,4 +79,4 @@ function viewBuild(file) {
 
 var infoView = viewBuild("./views/info/index.tsx");
 
-await Promise.all[(client, infoView)];
+await Promise.all[(node, browser, infoView)];

editor/code/package.json

@@ -290,7 +290,8 @@
     "vscode-languageclient": "^8.1.0",
     "vscode-languageserver-types": "^3.17.3"
   },
-  "main": "./out/src/client.js",
+  "main": "./out/src/node.js",
+  "browser": "/out/src/browser.js",
   "scripts": {
     "vscode:prepublish": "npm run typecheck && npm run esbuild -- --minify --sourcemap=no",
     "esbuild": "node esbuild.mjs",

editor/code/src/browser.ts

@@ -0,0 +1,22 @@
+import { ExtensionContext } from "vscode";
+import { LanguageClient } from "vscode-languageclient/browser";
+import { activateCoqLSP, ClientFactoryType, deactivateCoqLSP } from "./client";
+
+export function activate(context: ExtensionContext): void {
+  const cf: ClientFactoryType = (context, clientOptions, wsConfig) => {
+    // Pending on having the API to fetch the worker file.
+    throw "Worker not found";
+    let worker = new Worker("");
+    return new LanguageClient(
+      "coq-lsp",
+      "Coq LSP Worker",
+      clientOptions,
+      worker
+    );
+  };
+  activateCoqLSP(context, cf);
+}
+
+export function deactivate() {
+  deactivateCoqLSP();
+}

editor/code/src/client.ts

@@ -10,15 +10,14 @@ import {
   StatusBarAlignment,
   StatusBarItem,
   ThemeColor,
+  WorkspaceConfiguration,
 } from "vscode";
+
 import {
-  LanguageClient,
-  ServerOptions,
+  BaseLanguageClient,
   LanguageClientOptions,
-  RevealOutputChannelOn,
-} from "vscode-languageclient/node";
-import {
   RequestType,
+  RevealOutputChannelOn,
   VersionedTextDocumentIdentifier,
 } from "vscode-languageclient";
 import {
@@ -31,15 +30,24 @@ import { InfoPanel } from "./goals";
 import { FileProgressManager } from "./progress";
 
 let config: CoqLspClientConfig;
-let client: LanguageClient;
+let client: BaseLanguageClient;
 // Lifetime of the info panel == extension lifetime.
 let infoPanel: InfoPanel;
 // Lifetime of the fileProgress setup == client lifetime
 let fileProgress: FileProgressManager;
 // Status Bar Button
 let lspStatusItem: StatusBarItem;
 
-export function activate(context: ExtensionContext): void {
+export type ClientFactoryType = (
+  context: ExtensionContext,
+  clientOptions: LanguageClientOptions,
+  wsConfig: WorkspaceConfiguration
+) => BaseLanguageClient;
+
+export function activateCoqLSP(
+  context: ExtensionContext,
+  clientFactory: ClientFactoryType
+): void {
   window.showInformationMessage("Coq LSP Extension: Going to activate!");
 
   function coqCommand(command: string, fn: () => void) {
@@ -111,35 +119,30 @@ export function activate(context: ExtensionContext): void {
       initializationOptions,
       markdown: { isTrusted: true, supportHtml: true },
     };
-    const serverOptions: ServerOptions = {
-      command: wsConfig.path,
-      args: wsConfig.args,
-    };
 
-    client = new LanguageClient(
-      "coq-lsp",
-      "Coq LSP Server",
-      serverOptions,
-      clientOptions
-    );
+    let cP = new Promise<BaseLanguageClient>((resolve) => {
+      client = clientFactory(context, clientOptions, wsConfig);
+      fileProgress = new FileProgressManager(client);
+      resolve(client);
+    });
 
-    fileProgress = new FileProgressManager(client);
-    client
-      .start()
-      .then(updateStatusBar)
-      .then(() => {
-        if (window.activeTextEditor) {
-          goalsCall(
-            window.activeTextEditor,
-            TextEditorSelectionChangeKind.Command
-          );
-        }
-      })
-      .catch((error) => {
-        let emsg = error.toString();
-        console.log(`Error in coq-lsp start: ${emsg}`);
-        setFailedStatuBar(emsg);
-      });
+    cP.then((client) =>
+      client
+        .start()
+        .then(updateStatusBar)
+        .then(() => {
+          if (window.activeTextEditor) {
+            goalsCall(
+              window.activeTextEditor,
+              TextEditorSelectionChangeKind.Command
+            );
+          }
+        })
+    ).catch((error) => {
+      let emsg = error.toString();
+      console.log(`Error in coq-lsp start: ${emsg}`);
+      setFailedStatuBar(emsg);
+    });
   };
 
   const restart = () => {
@@ -294,7 +297,7 @@ export function activate(context: ExtensionContext): void {
 
   start();
 }
-export function deactivate(): Thenable<void> | undefined {
+export function deactivateCoqLSP(): Thenable<void> | undefined {
   if (!client) {
     return undefined;
   }

editor/code/src/goals.ts

@@ -1,9 +1,9 @@
 import { Position, Uri, WebviewPanel, window, ViewColumn } from "vscode";
 import {
+  BaseLanguageClient,
   RequestType,
   VersionedTextDocumentIdentifier,
 } from "vscode-languageclient";
-import { LanguageClient } from "vscode-languageclient/node";
 import { GoalRequest, GoalAnswer, PpString } from "../lib/types";
 
 const infoReq = new RequestType<GoalRequest, GoalAnswer<PpString>, void>(
@@ -86,7 +86,7 @@ export class InfoPanel {
   }
 
   // LSP Protocol extension for Goals
-  sendGoalsRequest(client: LanguageClient, params: GoalRequest) {
+  sendGoalsRequest(client: BaseLanguageClient, params: GoalRequest) {
     this.requestSent(params);
     client.sendRequest(infoReq, params).then(
       (goals) => this.requestDisplay(goals),
@@ -95,7 +95,7 @@ export class InfoPanel {
   }
 
   updateFromServer(
-    client: LanguageClient,
+    client: BaseLanguageClient,
     uri: Uri,
     version: number,
     position: Position

editor/code/src/node.ts

@@ -0,0 +1,23 @@
+import { ExtensionContext } from "vscode";
+import { LanguageClient, ServerOptions } from "vscode-languageclient/node";
+import { activateCoqLSP, ClientFactoryType, deactivateCoqLSP } from "./client";
+
+export function activate(context: ExtensionContext): void {
+  const cf: ClientFactoryType = (context, clientOptions, wsConfig) => {
+    const serverOptions: ServerOptions = {
+      command: wsConfig.path,
+      args: wsConfig.args,
+    };
+    return new LanguageClient(
+      "coq-lsp",
+      "Coq LSP Server",
+      serverOptions,
+      clientOptions
+    );
+  };
+  return activateCoqLSP(context, cf);
+}
+
+export function deactivate() {
+  return deactivateCoqLSP();
+}

editor/code/src/progress.ts

@@ -4,7 +4,7 @@ import {
   NotificationType,
   VersionedTextDocumentIdentifier,
 } from "vscode-languageclient";
-import { LanguageClient } from "vscode-languageclient/node";
+import { BaseLanguageClient } from "vscode-languageclient";
 
 enum CoqFileProgressKind {
   Processing = 1,
@@ -42,7 +42,7 @@ const progressDecoration = window.createTextEditorDecorationType({
 export class FileProgressManager {
   private fileProgress: Disposable;
 
-  constructor(client: LanguageClient) {
+  constructor(client: BaseLanguageClient) {
     this.fileProgress = client.onNotification(coqFileProgress, (params) => {
       let ranges = params.processing
         .map((fp) => client.protocol2CodeConverter.asRange(fp.range))