fix: "verified up to" bar no longer gets stuck (minor refactor)

__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<MessageHandlerEditor> {
+    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();
+        });
+    });
+});

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,95 +157,7 @@ window.onload = () => {
 	window.addEventListener("message", (event: MessageEvent<Message>) => {
 		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();
-					}
-					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} = 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;

editor/src/messageHandler.ts

@@ -0,0 +1,119 @@
+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<OffsetDiagnostic>) => 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:
+			// 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 {
+					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();
+					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:
+			// If we reach this 'default' case, then we have encountered an unknown message type.
+			console.log(`[WEBVIEW] Unrecognized message type '${msg.type}'`);
+			break;
+	}
+}