diff --git a/app/src/indexBrowser.tsx b/app/src/indexBrowser.tsx index 8f80a9d..ab3d243 100644 --- 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,10 +118,6 @@ 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; @@ -128,12 +125,7 @@ function Main() { 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 index ce91ac7..9ef0f30 100644 --- 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 index 2a4313a..e1b85f9 100644 Binary files a/extension/paperproof-0.0.4.vsix and b/extension/paperproof-0.0.4.vsix differ diff --git a/extension/src/extension.ts b/extension/src/extension.ts index c08d0d4..235390a 100644 --- 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 ` @@ -64,23 +71,25 @@ function getWebviewContent() {