From 8e7e1f7a8eeb5a35b65ec6ea66707ca86b8a3894 Mon Sep 17 00:00:00 2001 From: BenjiB Date: Mon, 30 Mar 2026 11:06:56 +0000 Subject: [PATCH 1/3] fix: "verified up to" bar no longer gets stuck --- editor/src/index.ts | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/editor/src/index.ts b/editor/src/index.ts index c4bd0abe..16fadfd5 100644 --- a/editor/src/index.ts +++ b/editor/src/index.ts @@ -206,14 +206,12 @@ window.onload = () => { break; case MessageType.progress: { - const {numberOfLines, progress} = msg.body; + const { numberOfLines, progress } = msg.body; if (progress.length === 0) { editor.removeBusyIndicators(); - } - const at = progress[0].range.start.line + 1; - if (at === numberOfLines) { - editor.reportProgress(at, numberOfLines, "File verified"); + editor.reportProgress(numberOfLines, numberOfLines, "File verified"); } else { + const at = progress[0].range.start.line + 1; editor.reportProgress(at, numberOfLines, `Verified file up to line: ${at}`); } break; From abaa3dad8a1b0598fac05e080c909ac2497abf13 Mon Sep 17 00:00:00 2001 From: BenjiB Date: Mon, 13 Apr 2026 17:20:48 +0000 Subject: [PATCH 2/3] extract messages send to editor into separate file and added tests for non-trivial cases --- __tests__/editor/messageHandler.test.ts | 143 ++++++++++++++++++++++++ editor/src/index.ts | 89 +-------------- editor/src/messageHandler.ts | 115 +++++++++++++++++++ 3 files changed, 260 insertions(+), 87 deletions(-) create mode 100644 __tests__/editor/messageHandler.test.ts create mode 100644 editor/src/messageHandler.ts diff --git a/__tests__/editor/messageHandler.test.ts b/__tests__/editor/messageHandler.test.ts new file mode 100644 index 00000000..d8495126 --- /dev/null +++ b/__tests__/editor/messageHandler.test.ts @@ -0,0 +1,143 @@ +import { Message, MessageType } from "../../shared"; +import { handleEditorMessage, MessageHandlerEditor } from "../../editor/src/messageHandler"; + +function createEditorMock(): jest.Mocked { + return { + init: jest.fn(), + insertSymbol: jest.fn(), + handleSnippet: jest.fn(), + replaceRange: jest.fn(), + handleCompletions: jest.fn(), + setInputAreaStatus: jest.fn(), + setShowLineNumbers: jest.fn(), + setShowMenuItems: jest.fn(), + handleHistoryChange: jest.fn(), + updateLockingState: jest.fn(), + removeBusyIndicators: jest.fn(), + reportProgress: jest.fn(), + setBusyIndicator: jest.fn(), + setActiveDiagnostics: jest.fn(), + startSpinner: jest.fn(), + stopSpinner: jest.fn(), + updateNodeViewThemes: jest.fn(), + }; +} + +describe("handleEditorMessage", () => { + describe("insert", () => { + it("calls handleSnippet for tactics type, not insertSymbol", () => { + const editor = createEditorMock(); + const msg: Message = { + type: MessageType.insert, + body: { symbolUnicode: "intro", type: "tactics", time: 1 }, + }; + + handleEditorMessage(editor, msg); + + expect(editor.handleSnippet).toHaveBeenCalledWith("intro"); + expect(editor.insertSymbol).not.toHaveBeenCalled(); + }); + + it("calls insertSymbol for non-tactics type, not handleSnippet", () => { + const editor = createEditorMock(); + const msg: Message = { + type: MessageType.insert, + body: { symbolUnicode: "∀", type: "symbol", time: 1 }, + }; + + handleEditorMessage(editor, msg); + + expect(editor.insertSymbol).toHaveBeenCalledWith("∀"); + expect(editor.handleSnippet).not.toHaveBeenCalled(); + }); + + it("aborts silently when tactics type has no symbolUnicode", () => { + const editor = createEditorMock(); + const msg = { + type: MessageType.insert, + body: { symbolUnicode: undefined, type: "tactics", time: 1 }, + } as unknown as Message; + + handleEditorMessage(editor, msg); + + expect(editor.handleSnippet).not.toHaveBeenCalled(); + expect(editor.insertSymbol).not.toHaveBeenCalled(); + }); + }); + + describe("progress", () => { + it("clears busy indicators and skips reportProgress when progress is empty", () => { + const editor = createEditorMock(); + const msg: Message = { + type: MessageType.progress, + body: { numberOfLines: 12, progress: [] }, + }; + + handleEditorMessage(editor, msg); + + expect(editor.removeBusyIndicators).toHaveBeenCalledTimes(1); + expect(editor.reportProgress).not.toHaveBeenCalled(); + }); + + it("reports 'File verified' when progress has reached the last line", () => { + const editor = createEditorMock(); + const numberOfLines = 50; + const msg: Message = { + type: MessageType.progress, + body: { + numberOfLines, + progress: [{ range: { start: { line: numberOfLines - 1, character: 0 }, end: { line: numberOfLines - 1, character: 0 } } }], + }, + }; + + handleEditorMessage(editor, msg); + + expect(editor.reportProgress).toHaveBeenCalledWith(numberOfLines, numberOfLines, "File verified"); + expect(editor.removeBusyIndicators).not.toHaveBeenCalled(); + }); + + it("reports partial progress message when not yet on the last line", () => { + const editor = createEditorMock(); + const msg: Message = { + type: MessageType.progress, + body: { + numberOfLines: 100, + progress: [{ range: { start: { line: 29, character: 0 }, end: { line: 29, character: 0 } } }], + }, + }; + + handleEditorMessage(editor, msg); + + expect(editor.reportProgress).toHaveBeenCalledWith(30, 100, expect.stringContaining("30")); + expect(editor.removeBusyIndicators).not.toHaveBeenCalled(); + }); + }); + + describe("serverStatus", () => { + it("starts spinner when status is Busy", () => { + const editor = createEditorMock(); + const msg: Message = { + type: MessageType.serverStatus, + body: { status: "Busy", metadata: "type-checking" }, + }; + + handleEditorMessage(editor, msg); + + expect(editor.startSpinner).toHaveBeenCalledTimes(1); + expect(editor.stopSpinner).not.toHaveBeenCalled(); + }); + + it("stops spinner when status is not Busy", () => { + const editor = createEditorMock(); + const msg: Message = { + type: MessageType.serverStatus, + body: { status: "Idle" }, + }; + + handleEditorMessage(editor, msg); + + expect(editor.stopSpinner).toHaveBeenCalledTimes(1); + expect(editor.startSpinner).not.toHaveBeenCalled(); + }); + }); +}); \ No newline at end of file diff --git a/editor/src/index.ts b/editor/src/index.ts index 16fadfd5..43f76b47 100644 --- a/editor/src/index.ts +++ b/editor/src/index.ts @@ -20,6 +20,7 @@ import * as langRocq from "@impermeable/codemirror-lang-rocq"; import { tagConfigurationLean } from "./leanFileConfiguration"; import { LeanSerializer } from "./leanSerializer"; import { versoMarkdownToMarkdown } from "./versoMarkdownSupport"; +import { handleEditorMessage } from "./messageHandler"; /** * Very basic representation of the acquirable VSCodeApi. @@ -156,93 +157,7 @@ window.onload = () => { window.addEventListener("message", (event: MessageEvent) => { const msg = event.data; - switch (msg.type) { - case MessageType.init: - editor.init(msg.body.value, msg.body.version); - break; - case MessageType.insert: - // Insert symbol message, retrieve the symbol from the message. - { - const { symbolUnicode } = msg.body; - if (msg.body.type === "tactics") { - // `symbolUnicode` stores the tactic template. - if (!symbolUnicode) { console.error("no template provided for snippet"); return; } - const template = symbolUnicode; - editor.handleSnippet(template); - } else { - editor.insertSymbol(symbolUnicode); - } - break; - } - case MessageType.replaceRange: - { - const { start, end, text } = msg.body; - editor.replaceRange(start, end, text); - break; - } - case MessageType.setAutocomplete: - // Handle autocompletion - editor.handleCompletions(msg.body); - break; - case MessageType.qedStatus: - { - const statuses = msg.body; // one status for each input area, in order - editor.setInputAreaStatus(statuses); - break; - } - case MessageType.setShowLineNumbers: - { - const show = msg.body; - editor.setShowLineNumbers(show); - break; - } - case MessageType.setShowMenuItems: - { const show = msg.body; editor.setShowMenuItems(show); break; } - case MessageType.editorHistoryChange: - editor.handleHistoryChange(msg.body); - break; - case MessageType.teacher: - editor.updateLockingState(msg.body); - break; - case MessageType.progress: - { - const { numberOfLines, progress } = msg.body; - if (progress.length === 0) { - editor.removeBusyIndicators(); - editor.reportProgress(numberOfLines, numberOfLines, "File verified"); - } else { - const at = progress[0].range.start.line + 1; - editor.reportProgress(at, numberOfLines, `Verified file up to line: ${at}`); - } - break; - } - case MessageType.executionInfo: - { - const range = msg.body; - editor.setBusyIndicator(range.from); - break; - } - case MessageType.diagnostics: - { editor.setActiveDiagnostics(msg.body.positionedDiagnostics); - break; } - case MessageType.serverStatus: - { - const {status} = msg.body; - if (status === "Busy") { - editor.startSpinner(); - } else { - editor.stopSpinner(); - } - break; - } - case MessageType.themeUpdate: - editor.updateNodeViewThemes(msg.body.theme); - break; - default: - // If we reach this 'default' case, then we have encountered an unknown message type. - console.log(`[WEBVIEW] Unrecognized message type '${msg.type}'`); - break; - } + handleEditorMessage(editor, msg); }); let timeoutHandle: number | undefined; diff --git a/editor/src/messageHandler.ts b/editor/src/messageHandler.ts new file mode 100644 index 00000000..c3c2beb0 --- /dev/null +++ b/editor/src/messageHandler.ts @@ -0,0 +1,115 @@ +import { Completion, HistoryChange, InputAreaStatus, OffsetDiagnostic, ThemeStyle } from "@impermeable/waterproof-editor"; +import { Message, MessageType, ServerStatus } from "../../shared"; + +export interface MessageHandlerEditor { + init: (value: string, version: number) => void; + insertSymbol: (symbolUnicode: string) => void; + handleSnippet: (template: string) => void; + replaceRange: (start: number, end: number, text: string) => void; + handleCompletions: (completions: Completion[]) => void; + setInputAreaStatus: (statuses: InputAreaStatus[]) => void; + setShowLineNumbers: (show: boolean) => void; + setShowMenuItems: (show: boolean) => void; + handleHistoryChange: (historyChange: HistoryChange) => void; + updateLockingState: (teacherModeEnabled: boolean) => void; + removeBusyIndicators: () => void; + reportProgress: (at: number, numberOfLines: number, label: string) => void; + setBusyIndicator: (from: number) => void; + setActiveDiagnostics: (diagnostics: Array) => void; + startSpinner: () => void; + stopSpinner: () => void; + updateNodeViewThemes: (theme: ThemeStyle) => void; +} + +export function handleEditorMessage(editor: MessageHandlerEditor, msg: Message): void { + switch (msg.type) { + case MessageType.init: + editor.init(msg.body.value, msg.body.version); + break; + case MessageType.insert: + { + const { symbolUnicode } = msg.body; + if (msg.body.type === "tactics") { + if (!symbolUnicode) { console.error("no template provided for snippet"); return; } + editor.handleSnippet(symbolUnicode); + } else { + editor.insertSymbol(symbolUnicode); + } + break; + } + case MessageType.replaceRange: + { + const { start, end, text } = msg.body; + editor.replaceRange(start, end, text); + break; + } + case MessageType.setAutocomplete: + editor.handleCompletions(msg.body); + break; + case MessageType.qedStatus: + { + const statuses = msg.body; + editor.setInputAreaStatus(statuses); + break; + } + case MessageType.setShowLineNumbers: + { + const show = msg.body; + editor.setShowLineNumbers(show); + break; + } + case MessageType.setShowMenuItems: + { + const show = msg.body; + editor.setShowMenuItems(show); + break; + } + case MessageType.editorHistoryChange: + editor.handleHistoryChange(msg.body); + break; + case MessageType.teacher: + editor.updateLockingState(msg.body); + break; + case MessageType.progress: + { + const { numberOfLines, progress } = msg.body; + if (progress.length === 0) { + editor.removeBusyIndicators(); + break; + } + + const at = progress[0].range.start.line + 1; + if (at === numberOfLines) { + editor.reportProgress(at, numberOfLines, "File verified"); + } else { + editor.reportProgress(at, numberOfLines, `Verified file up to line: ${at}`); + } + break; + } + case MessageType.executionInfo: + { + const range = msg.body; + editor.setBusyIndicator(range.from); + break; + } + case MessageType.diagnostics: + editor.setActiveDiagnostics(msg.body.positionedDiagnostics); + break; + case MessageType.serverStatus: + { + const status: ServerStatus = msg.body; + if (status.status === "Busy") { + editor.startSpinner(); + } else { + editor.stopSpinner(); + } + break; + } + case MessageType.themeUpdate: + editor.updateNodeViewThemes(msg.body.theme); + break; + default: + console.log(`[WEBVIEW] Unrecognized message type '${msg.type}'`); + break; + } +} From cf1be7b436133ea71477abd90513531ca35b47f9 Mon Sep 17 00:00:00 2001 From: BenjiB Date: Mon, 13 Apr 2026 17:33:00 +0000 Subject: [PATCH 3/3] added comments --- editor/src/messageHandler.ts | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/editor/src/messageHandler.ts b/editor/src/messageHandler.ts index c3c2beb0..e0681441 100644 --- a/editor/src/messageHandler.ts +++ b/editor/src/messageHandler.ts @@ -27,9 +27,11 @@ export function handleEditorMessage(editor: MessageHandlerEditor, msg: Message): editor.init(msg.body.value, msg.body.version); break; case MessageType.insert: + // Insert symbol message, retrieve the symbol from the message. { const { symbolUnicode } = msg.body; if (msg.body.type === "tactics") { + // `symbolUnicode` stores the tactic template. if (!symbolUnicode) { console.error("no template provided for snippet"); return; } editor.handleSnippet(symbolUnicode); } else { @@ -44,11 +46,12 @@ export function handleEditorMessage(editor: MessageHandlerEditor, msg: Message): break; } case MessageType.setAutocomplete: + // Handle autocompletion editor.handleCompletions(msg.body); break; case MessageType.qedStatus: { - const statuses = msg.body; + const statuses = msg.body; // one status for each input area, in order editor.setInputAreaStatus(statuses); break; } @@ -109,6 +112,7 @@ export function handleEditorMessage(editor: MessageHandlerEditor, msg: Message): editor.updateNodeViewThemes(msg.body.theme); break; default: + // If we reach this 'default' case, then we have encountered an unknown message type. console.log(`[WEBVIEW] Unrecognized message type '${msg.type}'`); break; }