Put initial info when creating webview html

Paper-Proof · Jul 21, 2023 · 55b62ff · 55b62ff
1 parent 43f323d
commit 55b62ff
Show file tree

Hide file tree

Showing 4 changed files with 63 additions and 36 deletions.
diff --git a/app/src/indexBrowser.tsx b/app/src/indexBrowser.tsx
@@ -15,6 +15,7 @@ import { useInterval } from "usehooks-ts";
 
 interface PaperProofWindow extends Window {
   sessionId: string | null;
+  initialInfo: string | null;
 }
 
 declare const window: PaperProofWindow;
@@ -117,23 +118,14 @@ function Main() {
   const BY_POST_MESSAGE = "by post message";
 
   useInterval(() => {
-    if (apiResponse && apiResponse.id == BY_POST_MESSAGE) {
-      // It runs as an extension and communicates changes directly
-      return;
-    }
     if (!sessionId) {
       // It runs as an extension
       return;
     }
     fetch(`${BASE_URL}/getTypes?sessionId=${sessionId}`)
       .then((response) => response.json())
       .then((newResponse) => {
-        if (
-          apiResponse &&
-          (apiResponse.id === BY_POST_MESSAGE ||
-            newResponse.id === apiResponse.id)
-        )
-          return;
+        if (apiResponse && newResponse.id === apiResponse.id) return;
         if (!app) return;
 
         // TODO: Errors from both server and extension should be handled uniformly
@@ -164,12 +156,17 @@ function Main() {
       console.log("Browser mode");
       setSessionId(window.sessionId);
     }
+    if (window.initialInfo) {
+      const newResponse: ApiResponse = {
+        ...JSON.parse(window.initialInfo),
+        id: BY_POST_MESSAGE,
+      };
+      updateUi(app, newResponse, apiResponse);
+      setApiResponse(newResponse);
+    }
 
     // Listen for direct messages from extension instead of round trip through server
     addEventListener("message", (event) => {
-      if (event.data["sessionId"]) {
-        setSessionId(event.data["sessionId"]);
-      }
       if (!app || !event.data["proofTree"]) return;
       const newResponse: ApiResponse = { ...event.data, id: BY_POST_MESSAGE };
 

diff --git a/extension/package.json b/extension/package.json
@@ -13,7 +13,9 @@
   "categories": [
     "Other"
   ],
-  "activationEvents": [],
+  "activationEvents": [
+    "onLanguage:lean4"
+  ],
   "main": "./dist/extension.js",
   "contributes": {
     "commands": [

diff --git a/extension/paperproof-0.0.4.vsix b/extension/paperproof-0.0.4.vsix
diff --git a/extension/src/extension.ts b/extension/src/extension.ts
@@ -6,6 +6,7 @@ import converter from "./converter";
 
 const SERVER_URL = "http://localhost:80";
 let sessionId: string | null = null;
+let latestInfo: object | null = null;
 
 const getErrorMessage = (error: unknown) => {
   if (error instanceof Error) {
@@ -14,21 +15,27 @@ const getErrorMessage = (error: unknown) => {
   return String(error);
 };
 
+const sendTypesToServer = async (sessionId: string, body: object) =>
+  fetch(`${SERVER_URL}/sendTypes?sessionId=${sessionId}`, {
+    method: "POST",
+    // eslint-disable-next-line @typescript-eslint/naming-convention
+    headers: { "Content-Type": "application/json" },
+    body: JSON.stringify(body),
+  });
+
 const sendTypes = async (
   webviewPanel: vscode.WebviewPanel | null,
   body: object
 ) => {
+  // Save for the later sending in case there is no session for the server or no webview open yet.
+  latestInfo = body;
+
   // 1. Send directly to the webview (if it's open!) to avoid lag
   webviewPanel?.webview.postMessage(body);
 
   // 2. After that, send data to .xyz
   if (sessionId) {
-    await fetch(`${SERVER_URL}/sendTypes?sessionId=${sessionId}`, {
-      method: "POST",
-      // eslint-disable-next-line @typescript-eslint/naming-convention
-      headers: { "Content-Type": "application/json" },
-      body: JSON.stringify(body),
-    });
+    sendTypesToServer(sessionId, body);
   }
 };
 
@@ -54,7 +61,7 @@ const vscodeRequest = async (
   return response;
 };
 
-function getWebviewContent() {
+function getWebviewContent(initialInfo: object | null) {
   return `
   <!DOCTYPE html>
   <html lang="en">
@@ -64,23 +71,25 @@ function getWebviewContent() {
       <title>Paperproof</title>
     </head>
     <body>
+      <script>initialInfo = ${
+        initialInfo ? JSON.stringify(initialInfo) : null
+      }</script>
       <div id="root"></div>
       <script src="${SERVER_URL}/indexBrowser.js"></script>
     </body>
   </html>`;
 }
 
-const onDidChangeTextEditorSelection = async (
+const sendInfoAtCurrentPos = async (
   log: vscode.OutputChannel,
   webviewPanel: vscode.WebviewPanel | null,
-  event: vscode.TextEditorSelectionChangeEvent
+  editor: vscode.TextEditor
 ) => {
-  const editor = event.textEditor;
   const doc = editor.document;
   if (doc.languageId !== "lean4" && doc.languageId !== "lean") {
     return;
   }
-  const pos = event.selections[0].active;
+  const pos = editor.selection.active;
   let tdp = {
     textDocument: { uri: doc.uri.toString() },
     position: { line: pos.line, character: pos.character },
@@ -129,15 +138,41 @@ const onDidChangeTextEditorSelection = async (
   log.appendLine("🎉 Sent everything");
 };
 
+function showNotification(sessionId: string) {
+  const url = `${SERVER_URL}/${sessionId}`;
+  const openButton: vscode.MessageItem = { title: "Open in browser" };
+  vscode.window
+    .showInformationMessage(`Your session is available at ${url}`, openButton)
+    .then((selectedItem) => {
+      if (selectedItem === openButton) {
+        vscode.env.openExternal(vscode.Uri.parse(url));
+      }
+    });
+}
+
 export function activate(context: vscode.ExtensionContext) {
   // Creates the 'paperproof' channel in vscode's "OUTPUT" pane
   let log = vscode.window.createOutputChannel("paperproof");
   let webviewPanel: vscode.WebviewPanel | null = null;
 
-  // 1. Sending types to the server on cursor changes.
+  // Creating a new paperproof working session
+  fetch(`${SERVER_URL}/newSession`, { method: "POST" })
+    .then((response) => response.json())
+    .then((res: any) => {
+      log.appendLine(`🎉 New session: ${res.sessionId}`);
+      sessionId = res.sessionId;
+      if (latestInfo) {
+        sendTypesToServer(res.sessionId, latestInfo).then(() => {
+          log.appendLine("🎉 Pending types sent");
+        });
+      }
+      showNotification(res.sessionId);
+    });
+
+  // Sending types to the server on cursor changes.
   vscode.window.onDidChangeTextEditorSelection(async (event) => {
     try {
-      await onDidChangeTextEditorSelection(log, webviewPanel, event);
+      await sendInfoAtCurrentPos(log, webviewPanel, event.textEditor);
     } catch (error) {
       const message = getErrorMessage(error);
       log.appendLine(
@@ -147,7 +182,7 @@ export function activate(context: vscode.ExtensionContext) {
     }
   });
 
-  // 2. Opening/hiding webviewPanel.
+  // Opening/hiding webviewPanel.
   function openPanel() {
     webviewPanel = vscode.window.createWebviewPanel(
       "paperproof",
@@ -158,14 +193,7 @@ export function activate(context: vscode.ExtensionContext) {
     webviewPanel.onDidDispose(() => {
       webviewPanel = null;
     });
-    webviewPanel.webview.html = getWebviewContent();
-    fetch(`${SERVER_URL}/newSession`, { method: "POST" })
-      .then((response) => response.json())
-      .then((res: any) => {
-        log.appendLine(`🎉 New session: ${res.sessionId}`);
-        sessionId = res.sessionId;
-        webviewPanel?.webview.postMessage({ sessionId: res.sessionId });
-      });
+    webviewPanel.webview.html = getWebviewContent(latestInfo);
   }
   const disposable = vscode.commands.registerCommand(
     "paperproof.toggle",